1 /-
2 Copyright (c) 2018 Kenny Lau. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Kenny Lau
5
6 Dependent functions with finite support (see `data/finsupp.lean`).
7 -/
8
9 import data.finset data.set.finite algebra.big_operators algebra.module algebra.pi_instances
src └─────────┘ └─────────────┘ └───────────────────┘ └────────────┘ └──────────────────┘
10
11 universes u u₁ u₂ v v₁ v₂ v₃ w x y l
12
13 variables (ι : Type u) (β : ι → Type v)
id └──┘ ┴
typ └──┘ ┴
14
15 def decidable_zero_symm {γ : Type w} [has_zero γ] [decidable_pred (eq (0 : γ))] : decidable_pred (λ x, x = (0:γ)) :=
id └──────┘ ┴ └────────────┘ └┘ ┴ └────────────┘ ┴ ┴ ┴ ┴
src └──────┘ └────────────┘ └┘ └────────────┘ ┴
typ └──────┘ ┴ └────────────┘ └┘ ┴ └────────────┘ ┴ ┴ ┴ ┴
16 λ x, decidable_of_iff (0 = x) eq_comm
id ┴ └──────────────┘ ┴ ┴ └─────┘
src └──────────────┘ ┴ └─────┘
typ ┴ └──────────────┘ ┴ ┴ └─────┘
17 local attribute [instance] decidable_zero_symm
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
18
19 namespace dfinsupp
20
21 variable [Π i, has_zero (β i)]
id ┴ └──────┘ ┴
src └──────┘
typ ┴ └──────┘ ┴
22
23 structure pre : Type (max u v) :=
24 (to_fun : Π i, β i)
id ┴ ┴ ┴
typ ┴ ┴ ┴
25 (pre_support : multiset ι)
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
26 (zero : ∀ i, i ∈ pre_support ∨ to_fun i = 0)
id ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ └─────────┘ ┴ └────┘ ┴ ┴
27
28 instance : setoid (pre ι β) :=
id └────┘ └─┘ ┴ ┴
src └────┘ └─┘
typ └────┘ └─┘ ┴ ┴
29 { r := λ x y, ∀ i, x.to_fun i = y.to_fun i,
id ┴ ┴ ┴ ┴└─────┘ ┴ ┴ ┴└─────┘ ┴
src └─────┘ ┴ └─────┘
typ ┴ ┴ ┴ ┴└─────┘ ┴ ┴ ┴└─────┘ ┴
30 iseqv := ⟨λ f i, rfl, λ f g H i, (H i).symm,
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
src └─┘ └──┘
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
31 λ f g h H1 H2 i, (H1 i).trans (H2 i)⟩ }
id ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └───┘ └┘ ┴
src └───┘
typ ┴ ┴ ┴ └┘ └┘ ┴ └┘ ┴ └───┘ └┘ ┴
32
33 end dfinsupp
34
35 variable {ι}
36 @[reducible] def dfinsupp [Π i, has_zero (β i)] : Type* :=
id ┴ └──────┘ ┴ ┴
src └──────┘
typ ┴ └──────┘ ┴ ┴
doc └───────┘
37 quotient (dfinsupp.setoid ι β)
id └──────┘ └─────────────┘ ┴ ┴
src └──────┘ └─────────────┘
typ └──────┘ └─────────────┘ ┴ ┴
38 variable {β}
39
40 notation `Π₀` binders `, ` r:(scoped f, dfinsupp f) := r
id └──────┘
src └──────┘
typ └──────┘
41 infix ` →ₚ `:25 := dfinsupp
id └──────┘
src └──────┘
typ └──────┘
42
43 namespace dfinsupp
44
45 section basic
46 variables [Π i, has_zero (β i)]
id ┴ └──────┘ ┴
src └──────┘
typ ┴ └──────┘ ┴
47 variables {β₁ : ι → Type v₁} {β₂ : ι → Type v₂}
id ┴
typ ┴
48 variables [Π i, has_zero (β₁ i)] [Π i, has_zero (β₂ i)]
id ┴ └──────┘ ┴ ┴ └──────┘ ┴
src └──────┘ └──────┘
typ ┴ └──────┘ ┴ ┴ └──────┘ ┴
49
50 instance : has_coe_to_fun (Π₀ i, β i) :=
id └────────────┘ └┘ ┴┴ ┴ ┴
src └────────────┘ └┘ ┴
typ └────────────┘ └┘ ┴┴ ┴ ┴
51 ⟨λ _, Π i, β i, λ f, quotient.lift_on f pre.to_fun $ λ _ _, funext⟩
id ┴ ┴ ┴ ┴ ┴ └──────────────┘ ┴ └────────┘ ┴ ┴ └────┘
src └──────────────┘ └────────┘ └────┘
typ ┴ ┴ ┴ ┴ ┴ └──────────────┘ ┴ └────────┘ ┴ ┴ └────┘
52
53 instance : has_zero (Π₀ i, β i) := ⟨⟦⟨λ i, 0, ∅, λ i, or.inr rfl⟩⟧⟩
id └──────┘ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └─┘ ┴
src └──────┘ └┘ ┴ ┴ ┴ └────┘ └─┘ ┴
typ └──────┘ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ └─┘ ┴
54 instance : inhabited (Π₀ i, β i) := ⟨0⟩
id └───────┘ └┘ ┴┴ ┴ ┴
src └───────┘ └┘ ┴
typ └───────┘ └┘ ┴┴ ┴ ┴
55
56 @[simp] lemma zero_apply {i : ι} : (0 : Π₀ i, β i) i = 0 := rfl
id ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ └─┘
src └┘ ┴ ┴ └─┘
typ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ └─┘
doc └──┘
57
58 @[ext]
doc └─┘
59 lemma ext {f g : Π₀ i, β i} (H : ∀ i, f i = g i) : f = g :=
id └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴
typ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
60 quotient.induction_on₂ f g (λ _ _ H, quotient.sound H) H
id └────────────────────┘ ┴ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └────────────────────┘ └────────────┘
typ └────────────────────┘ ┴ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
61
62 /-- The composition of `f : β₁ → β₂` and `g : Π₀ i, β₁ i` is
63 `map_range f hf g : Π₀ i, β₂ i`, well defined when `f 0 = 0`. -/
64 def map_range (f : Π i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0) (g : Π₀ i, β₁ i) : Π₀ i, β₂ i :=
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ └┘ ┴┴ └┘ ┴
src ┴ └┘ ┴ └┘ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ └┘ ┴┴ └┘ ┴
65 quotient.lift_on g (λ x, ⟦(⟨λ i, f i (x.1 i), x.2,
id └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └──────────────┘ ┴ ┴ ┴
typ └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
66 λ i, or.cases_on (x.3 i) or.inl $ λ H, or.inr $ by rw [H, hf]⟩ : pre ι β₂)⟧) $ λ x y H,
id ┴ └─────────┘ ┴┴ ┴ └────┘ ┴ └────┘ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴
src └─────────┘ ┴ └────┘ └────┘ └──┘ └┘ ┴ └─┘ ┴
typ ┴ └─────────┘ ┴┴ ┴ └────┘ ┴ └────┘ └──┘┴└┘└┘┴ └─┘ ┴ └┘ ┴ ┴ ┴ ┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └────┘└──┘┴
67 quotient.sound $ λ i, by simp only [H i]
id └────────────┘ ┴ ┴ ┴
src └────────────┘ └─────────┘ ┴ └─
typ └────────────┘ ┴ └─────────┘┴┴┴└─
doc └─────────┘ ┴ └─
txt └─────────┘ ┴ └─
par └─────────┘ ┴ └─
pid ┴└──┘└┘ ┴ ┴└
st └────────────────
68
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
69 @[simp] lemma map_range_apply
doc └──┘
70 {f : Π i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} {i : ι} :
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ ┴
src ┴ └┘ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ ┴
71 map_range f hf g i = f i (g i) :=
id └───────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
72 quotient.induction_on g $ λ x, rfl
id └───────────────────┘ ┴ ┴ └─┘
src └───────────────────┘ └─┘
typ └───────────────────┘ ┴ ┴ └─┘
73
74 def zip_with (f : Π i, β₁ i → β₂ i → β i) (hf : ∀ i, f i 0 0 = 0) (g₁ : Π₀ i, β₁ i) (g₂ : Π₀ i, β₂ i) : (Π₀ i, β i) :=
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ └┘ ┴┴ └┘ ┴ └┘ ┴┴ ┴ ┴
src ┴ └┘ ┴ └┘ ┴ └┘ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ └┘ ┴┴ └┘ ┴ └┘ ┴┴ ┴ ┴
75 begin
st └─────
76 refine quotient.lift_on₂ g₁ g₂ (λ x y, ⟦(⟨λ i, f i (x.1 i) (y.1 i), x.2 + y.2,
id └───────────────┘ └┘ └┘ ┴ ┴ ┴
src └─────┘└───────────────┘┴ ┴ ┴ └────┘┴ └──┘ ┴ ┴ └─┘ └┘ └─┘ └─┘ └─┘┴┴ └───
typ └─────┘└───────────────┘┴└┘┴└┘┴ └────┘┴ └──┘┴┴ ┴ └─┘ └┘ └─┘ └─┘ └─┘┴┴ └───
doc └─────┘ ┴ ┴ ┴ └────┘ └──┘ ┴ ┴ └─┘ └┘ └─┘ └─┘ └─┘ ┴ └───
txt └─────┘ ┴ ┴ ┴ └────┘ └──┘ ┴ ┴ └─┘ └┘ └─┘ └─┘ └─┘ ┴ └───
par └─────┘ ┴ ┴ ┴ └────┘ └──┘ ┴ ┴ └─┘ └┘ └─┘ └─┘ └─┘ ┴ └───
pid ┴ ┴ ┴ ┴ └────┘ └──┘ ┴ ┴ └─┘ └┘ └─┘ └─┘ └─┘ ┴ └───
st ─────────────────────────────────────────────────────────────────────────────────
77 λ i, _⟩ : pre ι β)⟧) _,
id └─┘ ┴ ┴ ┴
src ───┘ └───────┘└─┘┴ ┴ ┴┴└─┘
typ ───┘ └───────┘└─┘┴┴┴┴┴┴└─┘
doc ───┘ └───────┘ ┴ ┴ ┴ └─┘
txt ───┘ └───────┘ ┴ ┴ ┴ └─┘
par ───┘ └───────┘ ┴ ┴ ┴ └─┘
pid ───┘ └───────┘ ┴ ┴ ┴ └─┘
st ─────────────────────────┘└─
78 { cases x.3 i with h1 h1,
id ┴ ┴
src └────┘ └─┘ └─────────┘
typ └────┘┴└─┘┴└─────────┘
doc └────┘ └─┘ └─────────┘
txt └────┘ └─┘ └─────────┘
par └────┘ └─┘ └─────────┘
pid ┴ └─┘ └─────────┘
st ───┘└────────────────────┘└─
79 { left, rw multiset.mem_add, left, exact h1 },
id └──────────────┘ └┘
src └──┘ └─┘└──────────────┘ └──┘ └────┘ ┴
typ └──┘ └─┘└──────────────┘ └──┘ └────┘└┘┴
doc └──┘ └─┘ └──┘ └────┘ ┴
txt └──┘ └─┘ └──┘ └────┘ ┴
par └──┘ └─┘ └──┘ └────┘ ┴
pid ┴ ┴ ┴
st ─────┘└──┘└───────────────────┘└────┘└─────────┘└┘└
80 cases y.3 i with h2 h2,
id ┴ ┴
src └────┘ └─┘ └─────────┘
typ └────┘┴└─┘┴└─────────┘
doc └────┘ └─┘ └─────────┘
txt └────┘ └─┘ └─────────┘
par └────┘ └─┘ └─────────┘
pid ┴ └─┘ └─────────┘
st ─────────────────────────┘└─
81 { left, rw multiset.mem_add, right, exact h2 },
id └──────────────┘ └┘
src └──┘ └─┘└──────────────┘ └───┘ └────┘ ┴
typ └──┘ └─┘└──────────────┘ └───┘ └────┘└┘┴
doc └──┘ └─┘ └───┘ └────┘ ┴
txt └──┘ └─┘ └───┘ └────┘ ┴
par └──┘ └─┘ └───┘ └────┘ ┴
pid ┴ ┴ ┴
st ─────┘└──┘└───────────────────┘└─────┘└─────────┘└┘└
82 right, rw [h1, h2, hf] },
id └┘ └┘ └┘
src └───┘ └──┘ └┘ └┘ └┘
typ └───┘ └──┘└┘└┘└┘└┘└┘└┘
doc └───┘ └──┘ └┘ └┘ └┘
txt └───┘ └──┘ └┘ └┘ └┘
par └───┘ └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ────────┘└──────┘└──┘└──┘┴┴└┘└
83 exact λ x₁ x₂ y₁ y₂ H1 H2, quotient.sound $ λ i, by simp only [H1 i, H2 i]
id └────────────┘ └┘ ┴ └┘ ┴
src └────┘ └──────────────────┘└────────────┘┴ ┴ └──┘ ┴└─────────┘ ┴ └┘ ┴ └┘
typ └────┘ └──────────────────┘└────────────┘┴ ┴ └──┘ ┴└─────────┘└┘┴┴└┘└┘┴┴└┘
doc └────┘ └──────────────────┘ ┴ ┴ └──┘ ┴└─────────┘ ┴ └┘ ┴ └┘
txt └────┘ └──────────────────┘ ┴ ┴ └──┘ ┴└─────────┘ ┴ └┘ ┴ └┘
par └────┘ └──────────────────┘ ┴ ┴ └──┘ ┴└─────────┘ ┴ └┘ ┴ └┘
pid ┴ └──────────────────┘ ┴ ┴ └──┘ └──────────┘ ┴ └┘ ┴ └┘
st ────────────────────────────────────────────────────┘└──────────────────────┘
84 end
st └─┘
85
86 @[simp] lemma zip_with_apply
doc └──┘
87 {f : Π i, β₁ i → β₂ i → β i} {hf : ∀ i, f i 0 0 = 0} {g₁ : Π₀ i, β₁ i} {g₂ : Π₀ i, β₂ i} {i : ι} :
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴
src ┴ └┘ ┴ └┘ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴
88 zip_with f hf g₁ g₂ i = f i (g₁ i) (g₂ i) :=
id └──────┘ ┴ └┘ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴
src └──────┘ ┴
typ └──────┘ ┴ └┘ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴
89 quotient.induction_on₂ g₁ g₂ $ λ _ _, rfl
id └────────────────────┘ └┘ └┘ ┴ ┴ └─┘
src └────────────────────┘ └─┘
typ └────────────────────┘ └┘ └┘ ┴ ┴ └─┘
90
91 end basic
92
93 section algebra
94
95 instance [Π i, add_monoid (β i)] : has_add (Π₀ i, β i) :=
id ┴ └────────┘ ┴ ┴ └─────┘ └┘ ┴┴ ┴ ┴
src └────────┘ └─────┘ └┘ ┴
typ ┴ └────────┘ ┴ ┴ └─────┘ └┘ ┴┴ ┴ ┴
96 ⟨zip_with (λ _, (+)) (λ _, add_zero 0)⟩
id └──────┘ ┴ ┴ ┴ └──────┘
src └──────┘ ┴ └──────┘
typ └──────┘ ┴ ┴ ┴ └──────┘
97
98 @[simp] lemma add_apply [Π i, add_monoid (β i)] {g₁ g₂ : Π₀ i, β i} {i : ι} :
id ┴ └────────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴
src └────────┘ └┘ ┴
typ ┴ └────────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴
doc └──┘
99 (g₁ + g₂) i = g₁ i + g₂ i :=
id └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ ┴ ┴
typ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
100 zip_with_apply
id └────────────┘
src └────────────┘
typ └────────────┘
101
102 instance [Π i, add_monoid (β i)] : add_monoid (Π₀ i, β i) :=
id ┴ └────────┘ ┴ ┴ └────────┘ └┘ ┴┴ ┴ ┴
src └────────┘ └────────┘ └┘ ┴
typ ┴ └────────┘ ┴ ┴ └────────┘ └┘ ┴┴ ┴ ┴
103 { add_monoid .
104 zero := 0,
105 add := (+),
id ┴
src ┴
typ ┴
st ┴
106 add_assoc := λ f g h, ext $ λ i, by simp only [add_apply, add_assoc],
id ┴ ┴ ┴ └─┘ ┴ └───────┘ └───────┘
src └─┘ └─────────┘└───────┘└┘└───────┘┴
typ ┴ ┴ ┴ └─┘ ┴ └─────────┘└───────┘└┘└───────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └───────────────────────────────┘
107 zero_add := λ f, ext $ λ i, by simp only [add_apply, zero_apply, zero_add],
id ┴ └─┘ ┴ └───────┘ └────────┘ └──────┘
src └─┘ └─────────┘└───────┘└┘└────────┘└┘└──────┘┴
typ ┴ └─┘ ┴ └─────────┘└───────┘└┘└────────┘└┘└──────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st └──────────────────────────────────────────┘
108 add_zero := λ f, ext $ λ i, by simp only [add_apply, zero_apply, add_zero] }
id ┴ └─┘ ┴ └───────┘ └────────┘ └──────┘
src └─┘ └─────────┘└───────┘└┘└────────┘└┘└──────┘└┘
typ ┴ └─┘ ┴ └─────────┘└───────┘└┘└────────┘└┘└──────┘└┘
doc └─────────┘ └┘ └┘ └┘
txt └─────────┘ └┘ └┘ └┘
par └─────────┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ ┴┴
st └───────────────────────────────────────────┘
109
110 instance [Π i, add_monoid (β i)] {i : ι} : is_add_monoid_hom (λ g : Π₀ i : ι, β i, g i) :=
id ┴ └────────┘ ┴ ┴ ┴ └───────────────┘ └┘ ┴┴ ┴ ┴ ┴ ┴
src └────────┘ └───────────────┘ └┘ ┴
typ ┴ └────────┘ ┴ ┴ ┴ └───────────────┘ └┘ ┴┴ ┴ ┴ ┴ ┴
doc └───────────────┘
111 { map_add := λ _ _, add_apply, map_zero := zero_apply }
id ┴ ┴ └───────┘ └────────┘
src └───────┘ └────────┘
typ ┴ ┴ └───────┘ └────────┘
112
113 instance [Π i, add_group (β i)] : has_neg (Π₀ i, β i) :=
id ┴ └───────┘ ┴ ┴ └─────┘ └┘ ┴┴ ┴ ┴
src └───────┘ └─────┘ └┘ ┴
typ ┴ └───────┘ ┴ ┴ └─────┘ └┘ ┴┴ ┴ ┴
114 ⟨λ f, f.map_range (λ _, has_neg.neg) (λ _, neg_zero)⟩
id ┴ ┴└────────┘ ┴ └─────────┘ ┴ └──────┘
src └────────┘ └─────────┘ └──────┘
typ ┴ ┴└────────┘ ┴ └─────────┘ ┴ └──────┘
doc └────────┘
115
116 instance [Π i, add_comm_monoid (β i)] : add_comm_monoid (Π₀ i, β i) :=
id ┴ └─────────────┘ ┴ ┴ └─────────────┘ └┘ ┴┴ ┴ ┴
src └─────────────┘ └─────────────┘ └┘ ┴
typ ┴ └─────────────┘ ┴ ┴ └─────────────┘ └┘ ┴┴ ┴ ┴
117 { add_comm := λ f g, ext $ λ i, by simp only [add_apply, add_comm],
id ┴ ┴ └─┘ ┴ └───────┘ └──────┘
src └─┘ └─────────┘└───────┘└┘└──────┘┴
typ ┴ ┴ └─┘ ┴ └─────────┘└───────┘└┘└──────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └──────────────────────────────┘
118 .. dfinsupp.add_monoid }
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
119
120 @[simp] lemma neg_apply [Π i, add_group (β i)] {g : Π₀ i, β i} {i : ι} : (- g) i = - g i :=
id ┴ └───────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ └┘ ┴ ┴ ┴ ┴
typ ┴ └───────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
121 map_range_apply
id └─────────────┘
src └─────────────┘
typ └─────────────┘
122
123 instance [Π i, add_group (β i)] : add_group (Π₀ i, β i) :=
id ┴ └───────┘ ┴ ┴ └───────┘ └┘ ┴┴ ┴ ┴
src └───────┘ └───────┘ └┘ ┴
typ ┴ └───────┘ ┴ ┴ └───────┘ └┘ ┴┴ ┴ ┴
124 { add_left_neg := λ f, ext $ λ i, by simp only [add_apply, neg_apply, zero_apply, add_left_neg],
id ┴ └─┘ ┴ └───────┘ └───────┘ └────────┘ └──────────┘
src └─┘ └─────────┘└───────┘└┘└───────┘└┘└────────┘└┘└──────────┘┴
typ ┴ └─┘ ┴ └─────────┘└───────┘└┘└───────┘└┘└────────┘└┘└──────────┘┴
doc └─────────┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴
st └─────────────────────────────────────────────────────────┘
125 .. dfinsupp.add_monoid,
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
126 .. (infer_instance : has_neg (Π₀ i, β i)) }
id └────────────┘ └─────┘ └┘ ┴┴ ┴ ┴
src └────────────┘ └─────┘ └┘ ┴
typ └────────────┘ └─────┘ └┘ ┴┴ ┴ ┴
doc └────────────┘
127
128 @[simp] lemma sub_apply [Π i, add_group (β i)] {g₁ g₂ : Π₀ i, β i} {i : ι} : (g₁ - g₂) i = g₁ i - g₂ i :=
id ┴ └───────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └───────┘ └┘ ┴ ┴ ┴ ┴
typ ┴ └───────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └──┘
129 by rw [sub_eq_add_neg]; simp
id └────────────┘
src └──┘└────────────┘┴ └────
typ └──┘└────────────┘┴ └────
doc └──┘ ┴ └────
txt └──┘ ┴ └────
par └──┘ ┴ └────
pid └┘ ┴ └
st └─────────────────┘┴└──────
130
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
131 instance [Π i, add_comm_group (β i)] : add_comm_group (Π₀ i, β i) :=
id ┴ └────────────┘ ┴ ┴ └────────────┘ └┘ ┴┴ ┴ ┴
src └────────────┘ └────────────┘ └┘ ┴
typ ┴ └────────────┘ ┴ ┴ └────────────┘ └┘ ┴┴ ┴ ┴
132 { add_comm := λ f g, ext $ λ i, by simp only [add_apply, add_comm],
id ┴ ┴ └─┘ ┴ └───────┘ └──────┘
src └─┘ └─────────┘└───────┘└┘└──────┘┴
typ ┴ ┴ └─┘ ┴ └─────────┘└───────┘└┘└──────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └──────────────────────────────┘
133 ..dfinsupp.add_group }
id └────────────────┘
src └────────────────┘
typ └────────────────┘
134
135 def to_has_scalar {γ : Type w} [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)] : has_scalar γ (Π₀ i, β i) :=
id └──┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────────┘ ┴ └┘ ┴┴ ┴ ┴
src └──┘ └────────────┘ └────┘ └────────┘ └┘ ┴
typ └──┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────────┘ ┴ └┘ ┴┴ ┴ ┴
doc └────┘ └────────┘
136 ⟨λc v, v.map_range (λ _, (•) c) (λ _, smul_zero _)⟩
id ┴ ┴ ┴└────────┘ ┴ ┴ ┴ ┴ └───────┘
src └────────┘ ┴ └───────┘
typ ┴ ┴ ┴└────────┘ ┴ ┴ ┴ ┴ └───────┘
doc └────────┘
137 local attribute [instance] to_has_scalar
id └───────────┘
src └───────────┘
typ └───────────┘
138
139 @[simp] lemma smul_apply {γ : Type w} [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)] {i : ι} {b : γ} {v : Π₀ i, β i} :
id └──┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴
src └──┘ └────────────┘ └────┘ └┘ ┴
typ └──┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴
doc └──┘ └────┘
140 (b • v) i = b • (v i) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
141 map_range_apply
id └─────────────┘
src └─────────────┘
typ └─────────────┘
142
143 def to_module {γ : Type w} [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)] : module γ (Π₀ i, β i) :=
id └──┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ └┘ ┴┴ ┴ ┴
src └──┘ └────────────┘ └────┘ └────┘ └┘ ┴
typ └──┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ └┘ ┴┴ ┴ ┴
doc └────┘ └────┘
144 module.of_core {
id └────────────┘
src └────────────┘
typ └────────────┘
145 smul_add := λ c x y, ext $ λ i, by simp only [add_apply, smul_apply, smul_add],
id ┴ ┴ ┴ └─┘ ┴ └───────┘ └────────┘ └──────┘
src └─┘ └─────────┘└───────┘└┘└────────┘└┘└──────┘┴
typ ┴ ┴ ┴ └─┘ ┴ └─────────┘└───────┘└┘└────────┘└┘└──────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st └──────────────────────────────────────────┘
146 add_smul := λ c x y, ext $ λ i, by simp only [add_apply, smul_apply, add_smul],
id ┴ ┴ ┴ └─┘ ┴ └───────┘ └────────┘ └──────┘
src └─┘ └─────────┘└───────┘└┘└────────┘└┘└──────┘┴
typ ┴ ┴ ┴ └─┘ ┴ └─────────┘└───────┘└┘└────────┘└┘└──────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st └──────────────────────────────────────────┘
147 one_smul := λ x, ext $ λ i, by simp only [smul_apply, one_smul],
id ┴ └─┘ ┴ └────────┘ └──────┘
src └─┘ └─────────┘└────────┘└┘└──────┘┴
typ ┴ └─┘ ┴ └─────────┘└────────┘└┘└──────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └───────────────────────────────┘
148 mul_smul := λ r s x, ext $ λ i, by simp only [smul_apply, smul_smul],
id ┴ ┴ ┴ └─┘ ┴ └────────┘ └───────┘
src └─┘ └─────────┘└────────┘└┘└───────┘┴
typ ┴ ┴ ┴ └─┘ ┴ └─────────┘└────────┘└┘└───────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └────────────────────────────────┘
149 .. (infer_instance : has_scalar γ (Π₀ i, β i)) }
id └────────────┘ └────────┘ ┴ └┘ ┴┴ ┴ ┴
src └────────────┘ └────────┘ └┘ ┴
typ └────────────┘ └────────┘ ┴ └┘ ┴┴ ┴ ┴
doc └────────────┘ └────────┘
150
151 end algebra
152
153 section filter_and_subtype_domain
154
155 /-- `filter p f` is the function which is `f i` if `p i` is true and 0 otherwise. -/
156 def filter [Π i, has_zero (β i)] (p : ι → Prop) [decidable_pred p] (f : Π₀ i, β i) : Π₀ i, β i :=
id ┴ └──────┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ ┴┴ ┴ ┴ └┘ ┴┴ ┴ ┴
src └──────┘ └────────────┘ └┘ ┴ └┘ ┴
typ ┴ └──────┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ ┴┴ ┴ ┴ └┘ ┴┴ ┴ ┴
157 quotient.lift_on f (λ x, ⟦(⟨λ i, if p i then x.1 i else 0, x.2,
id └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └──────────────┘ ┴ ┴ ┴
typ └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
158 λ i, or.cases_on (x.3 i) or.inl $ λ H, or.inr $ by rw [H, if_t_t]⟩ : pre ι β)⟧) $ λ x y H,
id ┴ └─────────┘ ┴┴ ┴ └────┘ ┴ └────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────┘ ┴ └────┘ └────┘ └──┘ └┘└────┘┴ └─┘ ┴
typ ┴ └─────────┘ ┴┴ ┴ └────┘ ┴ └────┘ └──┘┴└┘└────┘┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └────┘└──────┘┴
159 quotient.sound $ λ i, by simp only [H i]
id └────────────┘ ┴ ┴ ┴
src └────────────┘ └─────────┘ ┴ └─
typ └────────────┘ ┴ └─────────┘┴┴┴└─
doc └─────────┘ ┴ └─
txt └─────────┘ ┴ └─
par └─────────┘ ┴ └─
pid ┴└──┘└┘ ┴ ┴└
st └────────────────
160
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
161 @[simp] lemma filter_apply [Π i, has_zero (β i)]
id ┴ └──────┘ ┴ ┴
src └──────┘
typ ┴ └──────┘ ┴ ┴
doc └──┘
162 {p : ι → Prop} [decidable_pred p] {i : ι} {f : Π₀ i, β i} :
id ┴ └────────────┘ ┴ ┴ └┘ ┴┴ ┴ ┴
src └────────────┘ └┘ ┴
typ ┴ └────────────┘ ┴ ┴ └┘ ┴┴ ┴ ┴
163 f.filter p i = if p i then f i else 0 :=
id ┴└─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴
typ ┴└─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
164 quotient.induction_on f $ λ x, rfl
id └───────────────────┘ ┴ ┴ └─┘
src └───────────────────┘ └─┘
typ └───────────────────┘ ┴ ┴ └─┘
165
166 @[simp] lemma filter_apply_pos [Π i, has_zero (β i)]
id ┴ └──────┘ ┴ ┴
src └──────┘
typ ┴ └──────┘ ┴ ┴
doc └──┘
167 {p : ι → Prop} [decidable_pred p] {f : Π₀ i, β i} {i : ι} (h : p i) :
id ┴ └────────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └────────────┘ └┘ ┴
typ ┴ └────────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
168 f.filter p i = f i :=
id ┴└─────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴
typ ┴└─────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘
169 by simp only [filter_apply, if_pos h]
id └──────────┘ └────┘ ┴
src └─────────┘└──────────┘└┘└────┘┴ └─
typ └─────────┘└──────────┘└┘└────┘┴┴└─
doc └─────────┘ └┘ ┴ └─
txt └─────────┘ └┘ ┴ └─
par └─────────┘ └┘ ┴ └─
pid ┴└──┘└┘ └┘ ┴ ┴└
st └───────────────────────────────────
170
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
171 @[simp] lemma filter_apply_neg [Π i, has_zero (β i)]
id ┴ └──────┘ ┴ ┴
src └──────┘
typ ┴ └──────┘ ┴ ┴
doc └──┘
172 {p : ι → Prop} [decidable_pred p] {f : Π₀ i, β i} {i : ι} (h : ¬ p i) :
id ┴ └────────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────┘ └┘ ┴ ┴
typ ┴ └────────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
173 f.filter p i = 0 :=
id ┴└─────┘ ┴ ┴ ┴
src └─────┘ ┴
typ ┴└─────┘ ┴ ┴ ┴
doc └─────┘
174 by simp only [filter_apply, if_neg h]
id └──────────┘ └────┘ ┴
src └─────────┘└──────────┘└┘└────┘┴ └─
typ └─────────┘└──────────┘└┘└────┘┴┴└─
doc └─────────┘ └┘ ┴ └─
txt └─────────┘ └┘ ┴ └─
par └─────────┘ └┘ ┴ └─
pid ┴└──┘└┘ └┘ ┴ ┴└
st └───────────────────────────────────
175
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
176 lemma filter_pos_add_filter_neg [Π i, add_monoid (β i)] {f : Π₀ i, β i}
id ┴ └────────┘ ┴ ┴ └┘ ┴┴ ┴ ┴
src └────────┘ └┘ ┴
typ ┴ └────────┘ ┴ ┴ └┘ ┴┴ ┴ ┴
177 {p : ι → Prop} [decidable_pred p] :
id ┴ └────────────┘ ┴
src └────────────┘
typ ┴ └────────────┘ ┴
178 f.filter p + f.filter (λi, ¬ p i) = f :=
id ┴└─────┘ ┴ ┴ ┴└─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ └─────┘ ┴ ┴
typ ┴└─────┘ ┴ ┴ ┴└─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘
179 ext $ λ i, by simp only [add_apply, filter_apply]; split_ifs; simp only [add_zero, zero_add]
id └─┘ ┴ └───────┘ └──────────┘ └──────┘ └──────┘
src └─┘ └─────────┘└───────┘└┘└──────────┘┴ └───────┘ └─────────┘└──────┘└┘└──────┘└─
typ └─┘ ┴ └─────────┘└───────┘└┘└──────────┘┴ └───────┘ └─────────┘└──────┘└┘└──────┘└─
doc └─────────┘ └┘ ┴ └───────┘ └─────────┘ └┘ └─
txt └─────────┘ └┘ ┴ └───────┘ └─────────┘ └┘ └─
par └─────────┘ └┘ ┴ └───────┘ └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴ ┴└──┘└┘ └┘ ┴└
st └───────────────────────────────────────────────────────────────────────────────
180
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
181 /-- `subtype_domain p f` is the restriction of the finitely supported function
182 `f` to the subtype `p`. -/
183 def subtype_domain [Π i, has_zero (β i)] (p : ι → Prop) [decidable_pred p]
id ┴ └──────┘ ┴ ┴ ┴ └────────────┘ ┴
src └──────┘ └────────────┘
typ ┴ └──────┘ ┴ ┴ ┴ └────────────┘ ┴
184 (f : Π₀ i, β i) : Π₀ i : subtype p, β i.1 :=
id └┘ ┴┴ ┴ ┴ └┘ └─────┘ ┴┴ ┴ ┴┴
src └┘ ┴ └┘ └─────┘ ┴ ┴
typ └┘ ┴┴ ┴ ┴ └┘ └─────┘ ┴┴ ┴ ┴┴
185 begin
st └─────
186 fapply quotient.lift_on f,
id └──────────────┘ ┴
src └─────┘└──────────────┘┴
typ └─────┘└──────────────┘┴┴
doc └─────┘ ┴
txt └─────┘ ┴
par └─────┘ ┴
pid ┴ ┴
st ──────────────────────────┘└─
187 { intro x, refine ⟦⟨λ i, x.1 i.1, (x.2.filter p).attach.map $ λ j, ⟨j.1, (multiset.mem_filter.1 j.2).2⟩, _⟩⟧,
id ┴ ┴ ┴ └─────────────────┘ ┴
src └─────┘ └─────┘┴ └──┘ └─┘ └──┘ └────────┘ └───────────┘ ┴ └──┘ └──┘ └─────────────────┘└─┘ └────────┘┴
typ └─────┘ └─────┘┴ └──┘ └─┘ └──┘ ┴└────────┘┴└───────────┘ ┴ └──┘ └──┘ └─────────────────┘└─┘ └────────┘┴
doc └─────┘ └─────┘ └──┘ └─┘ └──┘ └────────┘ └───────────┘ ┴ └──┘ └──┘ └─┘ └────────┘
txt └─────┘ └─────┘ └──┘ └─┘ └──┘ └────────┘ └───────────┘ ┴ └──┘ └──┘ └─┘ └────────┘
par └─────┘ └─────┘ └──┘ └─┘ └──┘ └────────┘ └───────────┘ ┴ └──┘ └──┘ └─┘ └────────┘
pid └┘ ┴ └──┘ └─┘ └──┘ └────────┘ └───────────┘ ┴ └──┘ └──┘ └─┘ └────────┘
st ───┘└─────┘└─────────────────────────────────────────────────────────────────────────────────────────────────┘└─
188 refine λ i, or.cases_on (x.3 i.1) (λ H, _) or.inr,
id └─────────┘ ┴ └────┘
src └─────┘ └──┘└─────────┘┴ └─┘ └──┘ └─────┘└────┘
typ └─────┘ └──┘└─────────┘┴ ┴└─┘ └──┘ └─────┘└────┘
doc └─────┘ └──┘ ┴ └─┘ └──┘ └─────┘
txt └─────┘ └──┘ ┴ └─┘ └──┘ └─────┘
par └─────┘ └──┘ ┴ └─┘ └──┘ └─────┘
pid ┴ └──┘ ┴ └─┘ └──┘ └─────┘
st ────────────────────────────────────────────────────┘└─
189 left, rw multiset.mem_map, refine ⟨⟨i.1, multiset.mem_filter.2 ⟨H, i.2⟩⟩, _, subtype.eta _ _⟩,
id └──────────────┘ └─────────────────┘ ┴ ┴ └─────────┘
src └──┘ └─┘└──────────────┘ └─────┘ └──┘└─────────────────┘└─┘ └┘ └───────┘└─────────┘└───┘
typ └──┘ └─┘└──────────────┘ └─────┘ └──┘└─────────────────┘└─┘ ┴└┘┴└───────┘└─────────┘└───┘
doc └──┘ └─┘ └─────┘ └──┘ └─┘ └┘ └───────┘ └───┘
txt └──┘ └─┘ └─────┘ └──┘ └─┘ └┘ └───────┘ └───┘
par └──┘ └─┘ └─────┘ └──┘ └─┘ └┘ └───────┘ └───┘
pid ┴ ┴ └──┘ └─┘ └┘ └───────┘ └───┘
st ───────┘└───────────────────┘└──────────────────────────────────────────────────────────────────┘└─
190 apply multiset.mem_attach },
id └─────────────────┘
src └────┘└─────────────────┘┴
typ └────┘└─────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────────┘└┘└
191 intros x y H,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └────┘
st ─────────────┘└─
192 exact quotient.sound (λ i, H i.1)
id └────────────┘ ┴
src └────┘└────────────┘┴ └──┘ ┴ └──┘
typ └────┘└────────────┘┴ └──┘┴┴ └──┘
doc └────┘ ┴ └──┘ ┴ └──┘
txt └────┘ ┴ └──┘ ┴ └──┘
par └────┘ ┴ └──┘ ┴ └──┘
pid ┴ ┴ └──┘ ┴ └─┘┴
st ───────────────────────────────────┘
193 end
st └─┘
194
195 @[simp] lemma subtype_domain_zero [Π i, has_zero (β i)] {p : ι → Prop} [decidable_pred p] :
id ┴ └──────┘ ┴ ┴ ┴ └────────────┘ ┴
src └──────┘ └────────────┘
typ ┴ └──────┘ ┴ ┴ ┴ └────────────┘ ┴
doc └──┘
196 subtype_domain p (0 : Π₀ i, β i) = 0 :=
id └────────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴
src └────────────┘ └┘ ┴ ┴
typ └────────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴
doc └────────────┘
197 rfl
id └─┘
src └─┘
typ └─┘
198
199 @[simp] lemma subtype_domain_apply [Π i, has_zero (β i)] {p : ι → Prop} [decidable_pred p]
id ┴ └──────┘ ┴ ┴ ┴ └────────────┘ ┴
src └──────┘ └────────────┘
typ ┴ └──────┘ ┴ ┴ ┴ └────────────┘ ┴
doc └──┘
200 {i : subtype p} {v : Π₀ i, β i} :
id └─────┘ ┴ └┘ ┴┴ ┴ ┴
src └─────┘ └┘ ┴
typ └─────┘ ┴ └┘ ┴┴ ┴ ┴
201 (subtype_domain p v) i = v (i.val) :=
id └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘
src └────────────┘ ┴ └──┘
typ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘
doc └────────────┘
202 quotient.induction_on v $ λ x, rfl
id └───────────────────┘ ┴ ┴ └─┘
src └───────────────────┘ └─┘
typ └───────────────────┘ ┴ ┴ └─┘
203
204 @[simp] lemma subtype_domain_add [Π i, add_monoid (β i)] {p : ι → Prop} [decidable_pred p] {v v' : Π₀ i, β i} :
id ┴ └────────┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ ┴┴ ┴ ┴
src └────────┘ └────────────┘ └┘ ┴
typ ┴ └────────┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ ┴┴ ┴ ┴
doc └──┘
205 (v + v').subtype_domain p = v.subtype_domain p + v'.subtype_domain p :=
id ┴ ┴ └┘ └────────────┘ ┴ ┴ ┴└─────────────┘ ┴ ┴ └┘└─────────────┘ ┴
src ┴ └────────────┘ ┴ └─────────────┘ ┴ └─────────────┘
typ ┴ ┴ └┘ └────────────┘ ┴ ┴ ┴└─────────────┘ ┴ ┴ └┘└─────────────┘ ┴
doc └────────────┘ └─────────────┘ └─────────────┘
206 ext $ λ i, by simp only [add_apply, subtype_domain_apply]
id └─┘ ┴ └───────┘ └──────────────────┘
src └─┘ └─────────┘└───────┘└┘└──────────────────┘└─
typ └─┘ ┴ └─────────┘└───────┘└┘└──────────────────┘└─
doc └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └────────────────────────────────────────────
207
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
208 instance subtype_domain.is_add_monoid_hom [Π i, add_monoid (β i)] {p : ι → Prop} [decidable_pred p] :
id ┴ └────────┘ ┴ ┴ ┴ └────────────┘ ┴
src └────────┘ └────────────┘
typ ┴ └────────┘ ┴ ┴ ┴ └────────────┘ ┴
209 is_add_monoid_hom (subtype_domain p : (Π₀ i : ι, β i) → Π₀ i : subtype p, β i) :=
id └───────────────┘ └────────────┘ ┴ └┘ ┴┴ ┴ ┴ └┘ └─────┘ ┴┴ ┴ ┴
src └───────────────┘ └────────────┘ └┘ ┴ └┘ └─────┘ ┴
typ └───────────────┘ └────────────┘ ┴ └┘ ┴┴ ┴ ┴ └┘ └─────┘ ┴┴ ┴ ┴
doc └───────────────┘ └────────────┘
210 { map_add := λ _ _, subtype_domain_add, map_zero := subtype_domain_zero }
id ┴ ┴ └────────────────┘ └─────────────────┘
src └────────────────┘ └─────────────────┘
typ ┴ ┴ └────────────────┘ └─────────────────┘
211
212 @[simp] lemma subtype_domain_neg [Π i, add_group (β i)] {p : ι → Prop} [decidable_pred p] {v : Π₀ i, β i} :
id ┴ └───────┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ ┴┴ ┴ ┴
src └───────┘ └────────────┘ └┘ ┴
typ ┴ └───────┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ ┴┴ ┴ ┴
doc └──┘
213 (- v).subtype_domain p = - v.subtype_domain p :=
id ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴└─────────────┘ ┴
src ┴ └────────────┘ ┴ ┴ └─────────────┘
typ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴└─────────────┘ ┴
doc └────────────┘ └─────────────┘
214 ext $ λ i, by simp only [neg_apply, subtype_domain_apply]
id └─┘ ┴ └───────┘ └──────────────────┘
src └─┘ └─────────┘└───────┘└┘└──────────────────┘└─
typ └─┘ ┴ └─────────┘└───────┘└┘└──────────────────┘└─
doc └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └────────────────────────────────────────────
215
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
216 @[simp] lemma subtype_domain_sub [Π i, add_group (β i)] {p : ι → Prop} [decidable_pred p] {v v' : Π₀ i, β i} :
id ┴ └───────┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ ┴┴ ┴ ┴
src └───────┘ └────────────┘ └┘ ┴
typ ┴ └───────┘ ┴ ┴ ┴ └────────────┘ ┴ └┘ ┴┴ ┴ ┴
doc └──┘
217 (v - v').subtype_domain p = v.subtype_domain p - v'.subtype_domain p :=
id ┴ ┴ └┘ └────────────┘ ┴ ┴ ┴└─────────────┘ ┴ ┴ └┘└─────────────┘ ┴
src ┴ └────────────┘ ┴ └─────────────┘ ┴ └─────────────┘
typ ┴ ┴ └┘ └────────────┘ ┴ ┴ ┴└─────────────┘ ┴ ┴ └┘└─────────────┘ ┴
doc └────────────┘ └─────────────┘ └─────────────┘
218 ext $ λ i, by simp only [sub_apply, subtype_domain_apply]
id └─┘ ┴ └───────┘ └──────────────────┘
src └─┘ └─────────┘└───────┘└┘└──────────────────┘└─
typ └─┘ ┴ └─────────┘└───────┘└┘└──────────────────┘└─
doc └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └────────────────────────────────────────────
219
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
220 end filter_and_subtype_domain
221
222
223 variable [decidable_eq ι]
id └──────────┘
src └──────────┘
typ └──────────┘
224
225 section basic
226 variable [Π i, has_zero (β i)]
id ┴ └──────┘ ┴
src └──────┘
typ ┴ └──────┘ ┴
227
228 lemma finite_supp (f : Π₀ i, β i) : set.finite {i | f i ≠ 0} :=
id └┘ ┴┴ ┴ ┴ └────────┘ ┴┴ ┴ ┴ ┴
src └┘ ┴ └────────┘ ┴ ┴
typ └┘ ┴┴ ┴ ┴ └────────┘ ┴┴ ┴ ┴ ┴
doc └────────┘
229 quotient.induction_on f $ λ x, set.finite_subset
id └───────────────────┘ ┴ ┴ └───────────────┘
src └───────────────────┘ └───────────────┘
typ └───────────────────┘ ┴ ┴ └───────────────┘
230 (finset.finite_to_set x.2.to_finset) $ λ i H,
id └──────────────────┘ ┴┴ └───────┘ ┴ ┴
src └──────────────────┘ ┴ └───────┘
typ └──────────────────┘ ┴┴ └───────┘ ┴ ┴
doc └───────┘
231 multiset.mem_to_finset.2 $ (x.3 i).resolve_right H
id └────────────────────┘┴ ┴┴ ┴ └───────────┘ ┴
src └────────────────────┘┴ ┴ └───────────┘
typ └────────────────────┘┴ ┴┴ ┴ └───────────┘ ┴
232
233 def mk (s : finset ι) (x : Π i : (↑s : set ι), β i.1) : Π₀ i, β i :=
id └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴ └┘ ┴┴ ┴ ┴
src └────┘ ┴ └─┘ ┴ └┘ ┴
typ └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴ └┘ ┴┴ ┴ ┴
doc └────┘
234 ⟦⟨λ i, if H : i ∈ s then x ⟨i, H⟩ else 0, s.1,
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
src ┴ └┘ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
235 λ i, if H : i ∈ s then or.inl H else or.inr $ dif_neg H⟩⟧
id ┴ └┘ ┴ ┴ ┴ └────┘ ┴ └────┘ ┴ └─────┘ ┴ ┴
src └┘ ┴ └────┘ └────┘ └─────┘ ┴
typ ┴ └┘ ┴ ┴ ┴ └────┘ ┴ └────┘ ┴ └─────┘ ┴ ┴
236
237 @[simp] lemma mk_apply {s : finset ι} {x : Π i : (↑s : set ι), β i.1} {i : ι} :
id └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴ ┴
src └────┘ ┴ └─┘ ┴
typ └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴ ┴
doc └──┘ └────┘
238 (mk s x : Π i, β i) i = if H : i ∈ s then x ⟨i, H⟩ else 0 :=
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └┘ ┴
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
239 rfl
id └─┘
src └─┘
typ └─┘
240
241 theorem mk_inj (s : finset ι) : function.injective (@mk ι β _ _ s) :=
id └────┘ ┴ └────────────────┘ └┘ ┴ ┴ ┴
src └────┘ └────────────────┘ └┘
typ └────┘ ┴ └────────────────┘ └┘ ┴ ┴ ┴
doc └────┘
242 begin
st └─────
243 intros x y H,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └────┘
st ─────────────┘└─
244 ext i,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
245 have h1 : (mk s x : Π i, β i) i = (mk s y : Π i, β i) i, {rw H},
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ ┴┴┴ └┘┴ ┴ └─┘ └┘ ┴ ┴ └┘ └─┘
typ └────────┘ ┴ ┴┴└─┘ └┘ ┴ ┴ └┘ ┴┴┴ └┘┴┴┴┴└─┘ └┘ ┴┴┴ └┘┴ └─┘┴
doc └────────┘ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ └─┘
txt └────────┘ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ └─┘
par └────────┘ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ └─┘
pid └─────┘└─┘ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └┘ ┴
st ────────────────────────────────────────────────────────┘└────┘┴└┘└
246 cases i with i hi,
id ┴
src └────┘ └────────┘
typ └────┘┴└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └────────┘
st ──────────────────┘└─
247 change i ∈ s at hi,
id ┴ ┴ ┴
src └─────┘ ┴┴┴ └────┘
typ └─────┘┴┴┴┴┴└────┘
doc └─────┘ ┴ ┴ └────┘
txt └─────┘ ┴ ┴ └────┘
par └─────┘ ┴ ┴ └────┘
pid ┴ ┴ ┴ ┴└───┘
st ───────────────────┘└─
248 dsimp only [mk_apply, subtype.coe_mk] at h1,
id └──────┘ └────────────┘
src └──────────┘└──────┘└┘└────────────┘└─────┘
typ └──────────┘└──────┘└┘└────────────┘└─────┘
doc └──────────┘ └┘ └─────┘
txt └──────────┘ └┘ └─────┘
par └──────────┘ └┘ └─────┘
pid └───┘└┘ └┘ ┴┴└───┘
st ────────────────────────────────────────────┘└─
249 simpa only [dif_pos hi] using h1
id └─────┘ └┘ └┘
src └──────────┘└─────┘┴ └──────┘ ┴
typ └──────────┘└─────┘┴└┘└──────┘└┘┴
doc └──────────┘ ┴ └──────┘ ┴
txt └──────────┘ ┴ └──────┘ ┴
par └──────────┘ ┴ └──────┘ ┴
pid ┴└──┘└┘ ┴ ┴┴└────┘ ┴
st ──────────────────────────────────┘
250 end
st └─┘
251
252 def single (i : ι) (b : β i) : Π₀ i, β i :=
id ┴ ┴ ┴ └┘ ┴┴ ┴ ┴
src └┘ ┴
typ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴
253 mk (finset.singleton i) $ λ j, eq.rec_on (finset.mem_singleton.1 j.2).symm b
id └┘ └──────────────┘ ┴ ┴ └───────┘ └──────────────────┘┴ ┴┴ └──┘ ┴
src └┘ └──────────────┘ └───────┘ └──────────────────┘┴ ┴ └──┘
typ └┘ └──────────────┘ ┴ ┴ └───────┘ └──────────────────┘┴ ┴┴ └──┘ ┴
doc └──────────────┘
254
255 @[simp] lemma single_apply {i i' b} : (single i b : Π₀ i, β i) i' = (if h : i = i' then eq.rec_on h b else 0) :=
id └────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ └───────┘ ┴ ┴ ┴
src └────┘ └┘ ┴ ┴ └┘ ┴ └───────┘
typ └────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ └───────┘ ┴ ┴ ┴
doc └──┘
256 begin
st └─────
257 dsimp only [single],
id └────┘
src └──────────┘└────┘┴
typ └──────────┘└────┘┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid └───┘└┘ ┴
st ────────────────────┘└─
258 by_cases h : i = i',
id ┴ ┴ └┘
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴└┘
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ────────────────────┘└─
259 { have h1 : i' ∈ finset.singleton i, { simp only [h, finset.mem_singleton] },
id └┘ ┴ └──────────────┘ ┴ ┴ └──────────────────┘
src └────────┘ ┴┴┴└──────────────┘┴ └─────────┘ └┘└──────────────────┘└┘
typ └────────┘└┘┴┴┴└──────────────┘┴┴ └─────────┘┴└┘└──────────────────┘└┘
doc └────────┘ ┴ ┴└──────────────┘┴ └─────────┘ └┘ └┘
txt └────────┘ ┴ ┴ ┴ └─────────┘ └┘ └┘
par └────────┘ ┴ ┴ ┴ └─────────┘ └┘ └┘
pid └─────┘└─┘ ┴ ┴ ┴ ┴└──┘└┘ └┘ ┴┴
st ───┘└───────────────────────────────┘└──┘└──────────────────────────────────┘└┘└
260 simp only [mk_apply, dif_pos h, dif_pos h1] },
id └──────┘ └─────┘ ┴ └─────┘ └┘
src └─────────┘└──────┘└┘└─────┘┴ └┘└─────┘┴ └┘
typ └─────────┘└──────┘└┘└─────┘┴┴└┘└─────┘┴└┘└┘
doc └─────────┘ └┘ ┴ └┘ ┴ └┘
txt └─────────┘ └┘ ┴ └┘ ┴ └┘
par └─────────┘ └┘ ┴ └┘ ┴ └┘
pid ┴└──┘└┘ └┘ ┴ └┘ ┴ ┴┴
st ───────────────────────────────────────────────┘└┘└
261 { have h1 : i' ∉ finset.singleton i, { simp only [ne.symm h, finset.mem_singleton, not_false_iff] },
id └┘ └──────────────┘ ┴ └─────┘ ┴ └──────────────────┘ └───────────┘
src └────────┘ ┴ ┴└──────────────┘┴ └─────────┘└─────┘┴ └┘└──────────────────┘└┘└───────────┘└┘
typ └────────┘└┘┴ ┴└──────────────┘┴┴ └─────────┘└─────┘┴┴└┘└──────────────────┘└┘└───────────┘└┘
doc └────────┘ ┴ ┴└──────────────┘┴ └─────────┘ ┴ └┘ └┘ └┘
txt └────────┘ ┴ ┴ ┴ └─────────┘ ┴ └┘ └┘ └┘
par └────────┘ ┴ ┴ ┴ └─────────┘ ┴ └┘ └┘ └┘
pid └─────┘└─┘ ┴ ┴ ┴ ┴└──┘└┘ ┴ └┘ └┘ ┴┴
st ────────────────────────────────────┘└──┘└─────────────────────────────────────────────────────────┘└┘└
262 simp only [mk_apply, dif_neg h, dif_neg h1] }
id └──────┘ └─────┘ ┴ └─────┘ └┘
src └─────────┘└──────┘└┘└─────┘┴ └┘└─────┘┴ └┘
typ └─────────┘└──────┘└┘└─────┘┴┴└┘└─────┘┴└┘└┘
doc └─────────┘ └┘ ┴ └┘ ┴ └┘
txt └─────────┘ └┘ ┴ └┘ ┴ └┘
par └─────────┘ └┘ ┴ └┘ ┴ └┘
pid ┴└──┘└┘ └┘ ┴ └┘ ┴ ┴┴
st ───────────────────────────────────────────────┘└─
263 end
st ──┘
264
265 @[simp] lemma single_zero {i} : (single i 0 : Π₀ i, β i) = 0 :=
id └────┘ ┴ └┘ ┴┴ ┴ ┴ ┴
src └────┘ └┘ ┴ ┴
typ └────┘ ┴ └┘ ┴┴ ┴ ┴ ┴
doc └──┘
266 quotient.sound $ λ j, if H : j ∈ finset.singleton i
id └────────────┘ ┴ └┘ ┴ ┴ └──────────────┘ ┴
src └────────────┘ └┘ ┴ └──────────────┘
typ └────────────┘ ┴ └┘ ┴ ┴ └──────────────┘ ┴
doc └──────────────┘
267 then by dsimp only; rw [dif_pos H]; cases finset.mem_singleton.1 H; refl
id └─────┘ ┴ └──────────────────┘ ┴
src └────────┘ └──┘└─────┘┴ ┴ └────┘└──────────────────┘└─┘ └───┘
typ └────────┘ └──┘└─────┘┴┴┴ └────┘└──────────────────┘└─┘┴ └───┘
doc └────────┘ └──┘ ┴ ┴ └────┘ └─┘ └───┘
txt └────────┘ └──┘ ┴ ┴ └────┘ └─┘ └───┘
par └────────┘ └──┘ ┴ ┴ └────┘ └─┘ └───┘
pid └───┘ └┘ ┴ ┴ ┴ └─┘ ┴
st └───────────────┘└───────┘┴└─────────────────────────────────────┘
268 else dif_neg H
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
269
270 @[simp] lemma single_eq_same {i b} : (single i b : Π₀ i, β i) i = b :=
id └────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └────┘ └┘ ┴ ┴
typ └────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
271 by simp only [single_apply, dif_pos rfl]
id └──────────┘ └─────┘ └─┘
src └─────────┘└──────────┘└┘└─────┘┴└─┘└─
typ └─────────┘└──────────┘└┘└─────┘┴└─┘└─
doc └─────────┘ └┘ ┴ └─
txt └─────────┘ └┘ ┴ └─
par └─────────┘ └┘ ┴ └─
pid ┴└──┘└┘ └┘ ┴ ┴└
st └──────────────────────────────────────
272
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
273 @[simp] lemma single_eq_of_ne {i i' b} (h : i ≠ i') : (single i b : Π₀ i, β i) i' = 0 :=
id ┴ ┴ └┘ └────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ └┘ ┴
src ┴ └────┘ └┘ ┴ ┴
typ ┴ ┴ └┘ └────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ └┘ ┴
doc └──┘
274 by simp only [single_apply, dif_neg h]
id └──────────┘ └─────┘ ┴
src └─────────┘└──────────┘└┘└─────┘┴ └─
typ └─────────┘└──────────┘└┘└─────┘┴┴└─
doc └─────────┘ └┘ ┴ └─
txt └─────────┘ └┘ ┴ └─
par └─────────┘ └┘ ┴ └─
pid ┴└──┘└┘ └┘ ┴ ┴└
st └────────────────────────────────────
275
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
276 def erase (i : ι) (f : Π₀ i, β i) : Π₀ i, β i :=
id ┴ └┘ ┴┴ ┴ ┴ └┘ ┴┴ ┴ ┴
src └┘ ┴ └┘ ┴
typ ┴ └┘ ┴┴ ┴ ┴ └┘ ┴┴ ┴ ┴
277 quotient.lift_on f (λ x, ⟦(⟨λ j, if j = i then 0 else x.1 j, x.2,
id └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src └──────────────┘ ┴ ┴ ┴ ┴
typ └──────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
278 λ j, or.cases_on (x.3 j) or.inl $ λ H, or.inr $ by simp only [H, if_t_t]⟩ : pre ι β)⟧) $ λ x y H,
id ┴ └─────────┘ ┴┴ ┴ └────┘ ┴ └────┘ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────┘ ┴ └────┘ └────┘ └─────────┘ └┘└────┘┴ └─┘ ┴
typ ┴ └─────────┘ ┴┴ ┴ └────┘ ┴ └────┘ └─────────┘┴└┘└────┘┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └────────────────────┘
279 quotient.sound $ λ j, if h : j = i then by simp only [if_pos h]
id └────────────┘ ┴ └┘ ┴ ┴ ┴ └────┘ ┴
src └────────────┘ └┘ ┴ └─────────┘└────┘┴ └┘
typ └────────────┘ ┴ └┘ ┴ ┴ ┴ └─────────┘└────┘┴┴└┘
doc └─────────┘ ┴ └┘
txt └─────────┘ ┴ └┘
par └─────────┘ ┴ └┘
pid ┴└──┘└┘ ┴ ┴┴
st └────────────────────┘
280 else by simp only [if_neg h, H j]
id └────┘ ┴ ┴ ┴
src └─────────┘└────┘┴ └┘ ┴ └─
typ └─────────┘└────┘┴┴└┘┴┴┴└─
doc └─────────┘ ┴ └┘ ┴ └─
txt └─────────┘ ┴ └┘ ┴ └─
par └─────────┘ ┴ └┘ ┴ └─
pid ┴└──┘└┘ ┴ └┘ ┴ ┴└
st └──────────────────────────
281
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
282 @[simp] lemma erase_apply {i j : ι} {f : Π₀ i, β i} :
id ┴ └┘ ┴┴ ┴ ┴
src └┘ ┴
typ ┴ └┘ ┴┴ ┴ ┴
doc └──┘
283 (f.erase i) j = if j = i then 0 else f j :=
id ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴
typ ┴└────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
284 quotient.induction_on f $ λ x, rfl
id └───────────────────┘ ┴ ┴ └─┘
src └───────────────────┘ └─┘
typ └───────────────────┘ ┴ ┴ └─┘
285
286 @[simp] lemma erase_same {i : ι} {f : Π₀ i, β i} : (f.erase i) i = 0 :=
id ┴ └┘ ┴┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴
src └┘ ┴ └────┘ ┴
typ ┴ └┘ ┴┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴
doc └──┘
287 by simp
src └────
typ └────
doc └────
txt └────
par └────
pid └
st └─────
288
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
289 @[simp] lemma erase_ne {i i' : ι} {f : Π₀ i, β i} (h : i' ≠ i) : (f.erase i) i' = f i' :=
id ┴ └┘ ┴┴ ┴ ┴ └┘ ┴ ┴ ┴└────┘ ┴ └┘ ┴ ┴ └┘
src └┘ ┴ ┴ └────┘ ┴
typ ┴ └┘ ┴┴ ┴ ┴ └┘ ┴ ┴ ┴└────┘ ┴ └┘ ┴ ┴ └┘
doc └──┘
290 by simp [h]
id ┴
src └────┘ └─
typ └────┘┴└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └─────────
291
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
292 end basic
293
294 section add_monoid
295
296 variable [Π i, add_monoid (β i)]
id ┴ └────────┘ ┴
src └────────┘
typ ┴ └────────┘ ┴
297
298 @[simp] lemma single_add {i : ι} {b₁ b₂ : β i} : single i (b₁ + b₂) = single i b₁ + single i b₂ :=
id ┴ ┴ ┴ └────┘ ┴ └┘ ┴ └┘ ┴ └────┘ ┴ └┘ ┴ └────┘ ┴ └┘
src └────┘ ┴ ┴ └────┘ ┴ └────┘
typ ┴ ┴ ┴ └────┘ ┴ └┘ ┴ └┘ ┴ └────┘ ┴ └┘ ┴ └────┘ ┴ └┘
doc └──┘
299 ext $ assume i',
id └─┘ └┘
src └─┘
typ └─┘ └┘
300 begin
st └─────
301 by_cases h : i = i',
id ┴ ┴ └┘
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴└┘
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ────────────────────┘└─
302 { subst h, simp only [add_apply, single_eq_same] },
id ┴ └───────┘ └────────────┘
src └────┘ └─────────┘└───────┘└┘└────────────┘└┘
typ └────┘┴ └─────────┘└───────┘└┘└────────────┘└┘
doc └────┘ └─────────┘ └┘ └┘
txt └────┘ └─────────┘ └┘ └┘
par └────┘ └─────────┘ └┘ └┘
pid ┴ ┴└──┘└┘ └┘ ┴┴
st ───┘└─────┘└──────────────────────────────────────┘└┘└
303 { simp only [add_apply, single_eq_of_ne h, zero_add] }
id └───────┘ └─────────────┘ ┴ └──────┘
src └─────────┘└───────┘└┘└─────────────┘┴ └┘└──────┘└┘
typ └─────────┘└───────┘└┘└─────────────┘┴┴└┘└──────┘└┘
doc └─────────┘ └┘ ┴ └┘ └┘
txt └─────────┘ └┘ ┴ └┘ └┘
par └─────────┘ └┘ ┴ └┘ └┘
pid ┴└──┘└┘ └┘ ┴ └┘ ┴┴
st ──────────────────────────────────────────────────────┘└─
304 end
st ──┘
305
306 lemma single_add_erase {i : ι} {f : Π₀ i, β i} : single i (f i) + f.erase i = f :=
id ┴ └┘ ┴┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴
src └┘ ┴ └────┘ ┴ └────┘ ┴
typ ┴ └┘ ┴┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴└────┘ ┴ ┴ ┴
307 ext $ λ i',
id └─┘ └┘
src └─┘
typ └─┘ └┘
308 if h : i = i' then by subst h; simp only [add_apply, single_apply, erase_apply, dif_pos rfl, if_pos, add_zero]
id └┘ ┴ ┴ └┘ ┴ └───────┘ └──────────┘ └─────────┘ └─────┘ └─┘ └────┘ └──────┘
src └┘ ┴ └────┘ └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘┴└─┘└┘└────┘└┘└──────┘└┘
typ └┘ ┴ ┴ └┘ └────┘┴ └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘┴└─┘└┘└────┘└┘└──────┘└┘
doc └────┘ └─────────┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘
txt └────┘ └─────────┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘
par └────┘ └─────────┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘
pid ┴ ┴└──┘└┘ └┘ └┘ └┘ ┴ └┘ └┘ ┴┴
st └────────────────────────────────────────────────────────────────────────────────────────┘
309 else by simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (ne.symm h), zero_add]
id └───────┘ └──────────┘ └─────────┘ └─────┘ ┴ └────┘ └─────┘ ┴ └──────┘
src └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘┴ └┘└────┘┴ └─────┘┴ └─┘└──────┘└─
typ └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘┴┴└┘└────┘┴ └─────┘┴┴└─┘└──────┘└─
doc └─────────┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴ └─┘ └─
txt └─────────┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴ └─┘ └─
par └─────────┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴ └─┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴ └─┘ ┴└
st └──────────────────────────────────────────────────────────────────────────────────────────
310
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
311 lemma erase_add_single {i : ι} {f : Π₀ i, β i} : f.erase i + single i (f i) = f :=
id ┴ └┘ ┴┴ ┴ ┴ ┴└────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └────┘ ┴ └────┘ ┴
typ ┴ └┘ ┴┴ ┴ ┴ ┴└────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
312 ext $ λ i',
id └─┘ └┘
src └─┘
typ └─┘ └┘
313 if h : i = i' then by subst h; simp only [add_apply, single_apply, erase_apply, dif_pos rfl, if_pos, zero_add]
id └┘ ┴ ┴ └┘ ┴ └───────┘ └──────────┘ └─────────┘ └─────┘ └─┘ └────┘ └──────┘
src └┘ ┴ └────┘ └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘┴└─┘└┘└────┘└┘└──────┘└┘
typ └┘ ┴ ┴ └┘ └────┘┴ └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘┴└─┘└┘└────┘└┘└──────┘└┘
doc └────┘ └─────────┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘
txt └────┘ └─────────┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘
par └────┘ └─────────┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘
pid ┴ ┴└──┘└┘ └┘ └┘ └┘ ┴ └┘ └┘ ┴┴
st └────────────────────────────────────────────────────────────────────────────────────────┘
314 else by simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (ne.symm h), add_zero]
id └───────┘ └──────────┘ └─────────┘ └─────┘ ┴ └────┘ └─────┘ ┴ └──────┘
src └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘┴ └┘└────┘┴ └─────┘┴ └─┘└──────┘└─
typ └─────────┘└───────┘└┘└──────────┘└┘└─────────┘└┘└─────┘┴┴└┘└────┘┴ └─────┘┴┴└─┘└──────┘└─
doc └─────────┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴ └─┘ └─
txt └─────────┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴ └─┘ └─
par └─────────┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴ └─┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ ┴ └┘ ┴ ┴ └─┘ ┴└
st └──────────────────────────────────────────────────────────────────────────────────────────
315
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
316 protected theorem induction {p : (Π₀ i, β i) → Prop} (f : Π₀ i, β i)
id └┘ ┴┴ ┴ ┴ └┘ ┴┴ ┴ ┴
src └┘ ┴ └┘ ┴
typ └┘ ┴┴ ┴ ┴ └┘ ┴┴ ┴ ┴
317 (h0 : p 0) (ha : ∀i b (f : Π₀ i, β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)) :
id ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ ┴ └────┘ ┴
typ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
318 p f :=
id ┴ ┴
typ ┴ ┴
319 begin
st └─────
320 refine quotient.induction_on f (λ x, _),
id └───────────────────┘ ┴
src └─────┘└───────────────────┘┴ ┴ └────┘
typ └─────┘└───────────────────┘┴┴┴ └────┘
doc └─────┘ ┴ ┴ └────┘
txt └─────┘ ┴ ┴ └────┘
par └─────┘ ┴ ┴ └────┘
pid ┴ ┴ ┴ └────┘
st ────────────────────────────────────────┘└─
321 cases x with f s H, revert f H,
id ┴
src └────┘ └─────────┘ └────────┘
typ └────┘┴└─────────┘ └────────┘
doc └────┘ └─────────┘ └────────┘
txt └────┘ └─────────┘ └────────┘
par └────┘ └─────────┘ └────────┘
pid ┴ └─────────┘ └──┘
st ───────────────────┘└──────────┘└─
322 apply multiset.induction_on s,
id └───────────────────┘ ┴
src └────┘└───────────────────┘┴
typ └────┘└───────────────────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────────┘└─
323 { intros f H, convert h0, ext i, exact (H i).resolve_left id },
id └┘ ┴ ┴ └┘
src └────────┘ └──────┘ └───┘ └────┘ ┴ └─────────────┘└┘┴
typ └────────┘ └──────┘└┘ └───┘ └────┘ ┴┴┴└─────────────┘└┘┴
doc └────────┘ └──────┘ └───┘ └────┘ ┴ └─────────────┘ ┴
txt └────────┘ └──────┘ └───┘ └────┘ ┴ └─────────────┘ ┴
par └────────┘ └──────┘ └───┘ └────┘ ┴ └─────────────┘ ┴
pid └──┘ ┴ └┘ ┴ ┴ └─────────────┘ ┴
st ───┘└────────┘└──────────┘└─────┘└────────────────────────────┘└┘└
324 intros i s ih f H,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └─────────┘
st ──────────────────┘└─
325 by_cases H1 : i ∈ s,
id ┴ ┴ ┴
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ────────────────────┘└─
326 { have H2 : ∀ j, j ∈ s ∨ f j = 0,
id ┴ ┴ ┴
src └────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴└┘
typ └────────┘ └┘ ┴ ┴ ┴┴┴ ┴┴┴ ┴┴└┘
doc └────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
txt └────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid └─────┘└─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
st ───┘└────────────────────────────┘└─
327 { intro j, cases H j with H2 H2,
id ┴ ┴
src └─────┘ └────┘ ┴ └─────────┘
typ └─────┘ └────┘┴┴┴└─────────┘
doc └─────┘ └────┘ ┴ └─────────┘
txt └─────┘ └────┘ ┴ └─────────┘
par └─────┘ └────┘ ┴ └─────────┘
pid └┘ ┴ ┴ └─────────┘
st ─────┘└─────┘└────────────────────┘└─
328 { cases multiset.mem_cons.1 H2 with H3 H3,
id └───────────────┘ └┘
src └────┘└───────────────┘└─┘ └─────────┘
typ └────┘└───────────────┘└─┘└┘└─────────┘
doc └────┘ └─┘ └─────────┘
txt └────┘ └─┘ └─────────┘
par └────┘ └─┘ └─────────┘
pid ┴ └─┘ └─────────┘
st ───────┘└─────────────────────────────────────┘└─
329 { left, rw H3, exact H1 },
id └┘ └┘
src └──┘ └─┘ └────┘ ┴
typ └──┘ └─┘└┘ └────┘└┘┴
doc └──┘ └─┘ └────┘ ┴
txt └──┘ └─┘ └────┘ ┴
par └──┘ └─┘ └────┘ ┴
pid ┴ ┴ ┴
st ─────────┘└──┘└─────┘└─────────┘└┘└
330 { left, exact H3 } },
id └┘
src └──┘ └────┘ ┴
typ └──┘ └────┘└┘┴
doc └──┘ └────┘ ┴
txt └──┘ └────┘ ┴
par └──┘ └────┘ ┴
pid ┴ ┴
st ─────────────┘└─────────┘└──┘└
331 right, exact H2 },
id └┘
src └───┘ └────┘ ┴
typ └───┘ └────┘└┘┴
doc └───┘ └────┘ ┴
txt └───┘ └────┘ ┴
par └───┘ └────┘ ┴
pid ┴ ┴
st ──────────┘└─────────┘└┘└
332 have H3 : (⟦{to_fun := f, pre_support := i :: s, zero := H}⟧ : Π₀ i, β i)
id ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └────────┘ ┴ └────────┘ └───────────────┘ ┴└┘┴ └────────┘ ┴┴└─┘└┘└┘┴┴ ┴ └─
typ └────────┘ ┴ └────────┘ └───────────────┘┴┴└┘┴ └────────┘┴┴┴└─┘└┘└┘┴┴┴┴ └─
doc └────────┘ └────────┘ └───────────────┘ ┴└┘┴ └────────┘ ┴ └─┘ └┘ ┴ ┴ └─
txt └────────┘ └────────┘ └───────────────┘ ┴ ┴ └────────┘ ┴ └─┘ └┘ ┴ ┴ └─
par └────────┘ └────────┘ └───────────────┘ ┴ ┴ └────────┘ ┴ └─┘ └┘ ┴ ┴ └─
pid └─────┘└─┘ └────────┘ └───────────────┘ ┴ ┴ └────────┘ ┴ └─┘ └┘ ┴ ┴ └─
st ──────────────────────────────────────────────────────────────────────────────
333 = ⟦{to_fun := f, pre_support := s, zero := H2}⟧,
id ┴ ┴ └┘
src ─────┘ ┴ └────────┘ └───────────────┘ └────────┘ ┴
typ ─────┘ ┴ └────────┘┴└───────────────┘┴└────────┘└┘┴
doc ─────┘ ┴ └────────┘ └───────────────┘ └────────┘ ┴
txt ─────┘ ┴ └────────┘ └───────────────┘ └────────┘ ┴
par ─────┘ ┴ └────────┘ └───────────────┘ └────────┘ ┴
pid ─────┘ ┴ └────────┘ └───────────────┘ └────────┘ ┴
st ────────────────────────────────────────────────────┘└─
334 { exact quotient.sound (λ i, rfl) },
id └────────────┘ └─┘
src └────┘└────────────┘┴ └──┘└─┘└┘
typ └────┘└────────────┘┴ └──┘└─┘└┘
doc └────┘ ┴ └──┘ └┘
txt └────┘ ┴ └──┘ └┘
par └────┘ ┴ └──┘ └┘
pid ┴ ┴ └──┘ ┴┴
st ─────┘└──────────────────────────────┘└┘└
335 rw H3, apply ih },
id └┘
src └─┘ └────┘ ┴
typ └─┘└┘ └────┘ ┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st ────────┘└─────────┘└┘└
336 have H2 : p (erase i ⟦{to_fun := f, pre_support := i :: s, zero := H}⟧),
id ┴ └───┘ ┴ ┴ ┴ ┴
src └────────┘ ┴ └───┘┴ ┴ └────────┘ └───────────────┘ ┴ ┴ └────────┘ ┴ ┴
typ └────────┘┴┴ └───┘┴ ┴ └────────┘┴└───────────────┘┴┴ ┴┴└────────┘┴┴ ┴
doc └────────┘ ┴ ┴ ┴ └────────┘ └───────────────┘ ┴ ┴ └────────┘ ┴ ┴
txt └────────┘ ┴ ┴ ┴ └────────┘ └───────────────┘ ┴ ┴ └────────┘ ┴ ┴
par └────────┘ ┴ ┴ ┴ └────────┘ └───────────────┘ ┴ ┴ └────────┘ ┴ ┴
pid └─────┘└─┘ ┴ ┴ ┴ └────────┘ └───────────────┘ ┴ ┴ └────────┘ ┴ ┴
st ────────────────────────────────────────────────────────────────────────┘└─
337 { dsimp only [erase, quotient.lift_on_beta],
id └───┘ └───────────────────┘
src └──────────┘└───┘└┘└───────────────────┘┴
typ └──────────┘└───┘└┘└───────────────────┘┴
doc └──────────┘ └┘ ┴
txt └──────────┘ └┘ ┴
par └──────────┘ └┘ ┴
pid └───┘└┘ └┘ ┴
st ───┘└───────────────────────────────────────┘└─
338 have H2 : ∀ j, j ∈ s ∨ ite (j = i) 0 (f j) = 0,
id ┴ └─┘ ┴ ┴
src └────────┘ └┘ ┴ ┴ ┴ ┴ ┴└─┘┴ ┴ ┴ └──┘ ┴ └┘ └┘
typ └────────┘ └┘ ┴ ┴ ┴┴┴ ┴└─┘┴ ┴ ┴┴└──┘ ┴┴ └┘ └┘
doc └────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ └┘
txt └────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ └┘
par └────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ └┘
pid └─────┘└─┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴┴
st ─────────────────────────────────────────────────┘└─
339 { intro j, cases H j with H2 H2,
id ┴ ┴
src └─────┘ └────┘ ┴ └─────────┘
typ └─────┘ └────┘┴┴┴└─────────┘
doc └─────┘ └────┘ ┴ └─────────┘
txt └─────┘ └────┘ ┴ └─────────┘
par └─────┘ └────┘ ┴ └─────────┘
pid └┘ ┴ ┴ └─────────┘
st ─────┘└─────┘└────────────────────┘└─
340 { cases multiset.mem_cons.1 H2 with H3 H3,
id └───────────────┘ └┘
src └────┘└───────────────┘└─┘ └─────────┘
typ └────┘└───────────────┘└─┘└┘└─────────┘
doc └────┘ └─┘ └─────────┘
txt └────┘ └─┘ └─────────┘
par └────┘ └─┘ └─────────┘
pid ┴ └─┘ └─────────┘
st ───────┘└─────────────────────────────────────┘└─
341 { right, exact if_pos H3 },
id └────┘ └┘
src └───┘ └────┘└────┘┴ ┴
typ └───┘ └────┘└────┘┴└┘┴
doc └───┘ └────┘ ┴ ┴
txt └───┘ └────┘ ┴ ┴
par └───┘ └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────┘└───┘└────────────────┘└┘└
342 { left, exact H3 } },
id └┘
src └──┘ └────┘ ┴
typ └──┘ └────┘└┘┴
doc └──┘ └────┘ ┴
txt └──┘ └────┘ ┴
par └──┘ └────┘ ┴
pid ┴ ┴
st ─────────────┘└─────────┘└──┘└
343 right, split_ifs; [refl, exact H2] },
id ┴ └┘
src └───┘ └───────┘ ┴└──┘ └────┘
typ └───┘ └───────┘ ┴└──┘ └────┘└┘
doc └───┘ └───────┘ └──┘ └────┘
txt └───┘ └───────┘ └──┘ └────┘
par └───┘ └───────┘ └──┘ └────┘
pid ┴
st ──────────┘└───────────────────────────┘└─┘└
344 have H3 : (⟦{to_fun := λ (j : ι), ite (j = i) 0 (f j), pre_support := i :: s, zero := _}⟧ : Π₀ i, β i)
id └┘ ┴ ┴
src └────────┘ └────────┘ └────┘ └─┘ ┴ ┴ ┴ └──┘ ┴ └────────────────┘ ┴ ┴ └──────────┘ └─┘└┘└┘┴┴ ┴ └─
typ └────────┘ └────────┘ └────┘ └─┘ ┴ ┴ ┴ └──┘ ┴ └────────────────┘ ┴ ┴ └──────────┘ └─┘└┘└┘┴┴┴┴ └─
doc └────────┘ └────────┘ └────┘ └─┘ ┴ ┴ ┴ └──┘ ┴ └────────────────┘ ┴ ┴ └──────────┘ └─┘ └┘ ┴ ┴ └─
txt └────────┘ └────────┘ └────┘ └─┘ ┴ ┴ ┴ └──┘ ┴ └────────────────┘ ┴ ┴ └──────────┘ └─┘ └┘ ┴ ┴ └─
par └────────┘ └────────┘ └────┘ └─┘ ┴ ┴ ┴ └──┘ ┴ └────────────────┘ ┴ ┴ └──────────┘ └─┘ └┘ ┴ ┴ └─
pid └─────┘└─┘ └────────┘ └────┘ └─┘ ┴ ┴ ┴ └──┘ ┴ └────────────────┘ ┴ ┴ └──────────┘ └─┘ └┘ ┴ ┴ └─
st ───────────────────────────────────────────────────────────────────────────────────────────────────────────
345 = ⟦{to_fun := λ (j : ι), ite (j = i) 0 (f j), pre_support := s, zero := H2}⟧ :=
id ┴ └─┘ ┴ ┴ ┴ └┘
src ─────┘ ┴ └────────┘ └────┘ └─┘└─┘┴ ┴ ┴ └──┘ ┴ └────────────────┘ └────────┘ ┴ └───
typ ─────┘ ┴ └────────┘ └────┘┴└─┘└─┘┴ ┴ ┴┴└──┘ ┴┴ └────────────────┘┴└────────┘└┘┴ └───
doc ─────┘ ┴ └────────┘ └────┘ └─┘ ┴ ┴ ┴ └──┘ ┴ └────────────────┘ └────────┘ ┴ └───
txt ─────┘ ┴ └────────┘ └────┘ └─┘ ┴ ┴ ┴ └──┘ ┴ └────────────────┘ └────────┘ ┴ └───
par ─────┘ ┴ └────────┘ └────┘ └─┘ ┴ ┴ ┴ └──┘ ┴ └────────────────┘ └────────┘ ┴ └───
pid ─────┘ ┴ └────────┘ └────┘ └─┘ ┴ ┴ ┴ └──┘ ┴ └────────────────┘ └────────┘ ┴ └───
st ──────────────────────────────────────────────────────────────────────────────────────
346 quotient.sound (λ i, rfl),
id └────────────┘ └─┘
src ─────┘└────────────┘┴ └──┘└─┘┴
typ ─────┘└────────────┘┴ └──┘└─┘┴
doc ─────┘ ┴ └──┘ ┴
txt ─────┘ ┴ └──┘ ┴
par ─────┘ ┴ └──┘ ┴
pid ─────┘ ┴ └──┘ ┴
st ──────────────────────────────┘└─
347 rw H3, apply ih },
id └┘
src └─┘ └────┘ ┴
typ └─┘└┘ └────┘ ┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st ────────┘└─────────┘└┘└
348 have H3 : single i _ + _ = (⟦{to_fun := f, pre_support := i :: s, zero := H}⟧ : Π₀ i, β i) := single_add_erase,
id └────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └──────────────┘
src └────────┘└────┘┴ └─┘┴└─┘ ┴ └────────┘ └───────────────┘ ┴ ┴ └────────┘ ┴ └─┘└┘└┘┴┴ ┴ └───┘└──────────────┘
typ └────────┘└────┘┴ └─┘┴└─┘ ┴ └────────┘┴└───────────────┘┴┴ ┴┴└────────┘┴┴ └─┘└┘└┘┴┴┴┴ └───┘└──────────────┘
doc └────────┘ ┴ └─┘ └─┘ ┴ └────────┘ └───────────────┘ ┴ ┴ └────────┘ ┴ └─┘ └┘ ┴ ┴ └───┘
txt └────────┘ ┴ └─┘ └─┘ ┴ └────────┘ └───────────────┘ ┴ ┴ └────────┘ ┴ └─┘ └┘ ┴ ┴ └───┘
par └────────┘ ┴ └─┘ └─┘ ┴ └────────┘ └───────────────┘ ┴ ┴ └────────┘ ┴ └─┘ └┘ ┴ ┴ └───┘
pid └─────┘└─┘ ┴ └─┘ └─┘ ┴ └────────┘ └───────────────┘ ┴ ┴ └────────┘ ┴ └─┘ └┘ ┴ ┴ ┴└──┘
st ───────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
349 rw ← H3,
id └┘
src └───┘
typ └───┘└┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ────────┘└─
350 change p (single i (f i) + _),
id ┴ └────┘ ┴ ┴
src └─────┘ ┴ └────┘┴ ┴ ┴ └┘ └─┘
typ └─────┘┴┴ └────┘┴ ┴ ┴┴┴└┘ └─┘
doc └─────┘ ┴ ┴ ┴ ┴ └┘ └─┘
txt └─────┘ ┴ ┴ ┴ ┴ └┘ └─┘
par └─────┘ ┴ ┴ ┴ ┴ └┘ └─┘
pid ┴ ┴ ┴ ┴ ┴ └┘ └─┘
st ──────────────────────────────┘└─
351 cases classical.em (f i = 0) with h h,
id └──────────┘ ┴ ┴
src └────┘└──────────┘┴ ┴ ┴ └──────────┘
typ └────┘└──────────┘┴ ┴┴┴┴ └──────────┘
doc └────┘ ┴ ┴ ┴ └──────────┘
txt └────┘ ┴ ┴ ┴ └──────────┘
par └────┘ ┴ ┴ ┴ └──────────┘
pid ┴ ┴ ┴ ┴ └─┘└───────┘
st ──────────────────────────────────────┘└─
352 { rw [h, single_zero, zero_add], exact H2 },
id ┴ └─────────┘ └──────┘ └┘
src └──┘ └┘└─────────┘└┘└──────┘┴ └────┘ ┴
typ └──┘┴└┘└─────────┘└┘└──────┘┴ └────┘└┘┴
doc └──┘ └┘ └┘ ┴ └────┘ ┴
txt └──┘ └┘ └┘ ┴ └────┘ ┴
par └──┘ └┘ └┘ ┴ └────┘ ┴
pid └┘ └┘ └┘ ┴ ┴ ┴
st ───┘└───┘└───────────┘└────────┘┴└─────────┘└┘└
353 refine ha _ _ _ _ h H2,
id └┘ ┴ └┘
src └─────┘ └───────┘ ┴
typ └─────┘└┘└───────┘┴┴└┘
doc └─────┘ └───────┘ ┴
txt └─────┘ └───────┘ ┴
par └─────┘ └───────┘ ┴
pid ┴ └───────┘ ┴
st ───────────────────────┘└─
354 rw erase_same
id └────────┘
src └─┘└────────┘┴
typ └─┘└────────┘┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ───────────────┘
355 end
st └─┘
356
357 lemma induction₂ {p : (Π₀ i, β i) → Prop} (f : Π₀ i, β i)
id └┘ ┴┴ ┴ ┴ └┘ ┴┴ ┴ ┴
src └┘ ┴ └┘ ┴
typ └┘ ┴┴ ┴ ┴ └┘ ┴┴ ┴ ┴
358 (h0 : p 0) (ha : ∀i b (f : Π₀ i, β i), f i = 0 → b ≠ 0 → p f → p (f + single i b)) :
id ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
src └┘ ┴ ┴ ┴ ┴ └────┘
typ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
359 p f :=
id ┴ ┴
typ ┴ ┴
360 dfinsupp.induction f h0 $ λ i b f h1 h2 h3,
id └────────────────┘ ┴ └┘ ┴ ┴ ┴ └┘ └┘ └┘
src └────────────────┘
typ └────────────────┘ ┴ └┘ ┴ ┴ ┴ └┘ └┘ └┘
361 have h4 : f + single i b = single i b + f,
id ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴ └────┘ ┴
typ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
362 { ext j, by_cases H : i = j,
id ┴ ┴ ┴
src └───┘ └───────┘ └─┘ ┴┴┴
typ └───┘ └───────┘ └─┘┴┴┴┴┴
doc └───┘ └───────┘ └─┘ ┴ ┴
txt └───┘ └───────┘ └─┘ ┴ ┴
par └───┘ └───────┘ └─┘ ┴ ┴
pid └┘ ┴ └─┘ ┴ ┴
st └─────┘└──────────────────┘└─
363 { subst H, simp [h1] },
id ┴ └┘
src └────┘ └────┘ └┘
typ └────┘┴ └────┘└┘└┘
doc └────┘ └────┘ └┘
txt └────┘ └────┘ └┘
par └────┘ └────┘ └┘
pid ┴ ┴┴ ┴┴
st ───┘└─────┘└──────────┘└┘└
364 { simp [H] } },
id ┴
src └────┘ └┘
typ └────┘┴└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ────────────┘└──┘
365 eq.rec_on h4 $ ha i b f h1 h2 h3
id └───────┘ └┘ └┘ ┴ ┴ ┴ └┘ └┘ └┘
src └───────┘
typ └───────┘ └┘ └┘ ┴ ┴ ┴ └┘ └┘ └┘
366
367 end add_monoid
368
369 @[simp] lemma mk_add [Π i, add_monoid (β i)] {s : finset ι} {x y : Π i : (↑s : set ι), β i.1} :
id ┴ └────────┘ ┴ ┴ └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴
src └────────┘ └────┘ ┴ └─┘ ┴
typ ┴ └────────┘ ┴ ┴ └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴
doc └──┘ └────┘
370 mk s (x + y) = mk s x + mk s y :=
id └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
src └┘ ┴ ┴ └┘ ┴ └┘
typ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
371 ext $ λ i, by simp only [add_apply, mk_apply]; split_ifs; [refl, rw zero_add]
id └─┘ ┴ └───────┘ └──────┘ ┴ └──────┘
src └─┘ └─────────┘└───────┘└┘└──────┘┴ └───────┘ ┴└──┘ └─┘└──────┘
typ └─┘ ┴ └─────────┘└───────┘└┘└──────┘┴ └───────┘ ┴└──┘ └─┘└──────┘
doc └─────────┘ └┘ ┴ └───────┘ └──┘ └─┘
txt └─────────┘ └┘ ┴ └───────┘ └──┘ └─┘
par └─────────┘ └┘ ┴ └───────┘ └──┘ └─┘
pid ┴└──┘└┘ └┘ ┴ ┴
st └─────────────────────────────────────────────────────┘└──────┘┴
372
373 @[simp] lemma mk_zero [Π i, has_zero (β i)] {s : finset ι} :
id ┴ └──────┘ ┴ ┴ └────┘ ┴
src └──────┘ └────┘
typ ┴ └──────┘ ┴ ┴ └────┘ ┴
doc └──┘ └────┘
374 mk s (0 : Π i : (↑s : set ι), β i.1) = 0 :=
id └┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴ ┴
src └┘ ┴ └─┘ ┴ ┴
typ └┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴ ┴
375 ext $ λ i, by simp only [mk_apply]; split_ifs; refl
id └─┘ ┴ └──────┘
src └─┘ └─────────┘└──────┘┴ └───────┘ └────
typ └─┘ ┴ └─────────┘└──────┘┴ └───────┘ └────
doc └─────────┘ ┴ └───────┘ └────
txt └─────────┘ ┴ └───────┘ └────
par └─────────┘ ┴ └───────┘ └────
pid ┴└──┘└┘ ┴ └
st └──────────────────────────────────────
376
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
377 @[simp] lemma mk_neg [Π i, add_group (β i)] {s : finset ι} {x : Π i : (↑s : set ι), β i.1} :
id ┴ └───────┘ ┴ ┴ └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴
src └───────┘ └────┘ ┴ └─┘ ┴
typ ┴ └───────┘ ┴ ┴ └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴
doc └──┘ └────┘
378 mk s (-x) = -mk s x :=
id └┘ ┴ ┴┴ ┴ ┴└┘ ┴ ┴
src └┘ ┴ ┴ ┴└┘
typ └┘ ┴ ┴┴ ┴ ┴└┘ ┴ ┴
379 ext $ λ i, by simp only [neg_apply, mk_apply]; split_ifs; [refl, rw neg_zero]
id └─┘ ┴ └───────┘ └──────┘ ┴ └──────┘
src └─┘ └─────────┘└───────┘└┘└──────┘┴ └───────┘ ┴└──┘ └─┘└──────┘
typ └─┘ ┴ └─────────┘└───────┘└┘└──────┘┴ └───────┘ ┴└──┘ └─┘└──────┘
doc └─────────┘ └┘ ┴ └───────┘ └──┘ └─┘
txt └─────────┘ └┘ ┴ └───────┘ └──┘ └─┘
par └─────────┘ └┘ ┴ └───────┘ └──┘ └─┘
pid ┴└──┘└┘ └┘ ┴ ┴
st └─────────────────────────────────────────────────────┘└──────┘┴
380
381 @[simp] lemma mk_sub [Π i, add_group (β i)] {s : finset ι} {x y : Π i : (↑s : set ι), β i.1} :
id ┴ └───────┘ ┴ ┴ └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴
src └───────┘ └────┘ ┴ └─┘ ┴
typ ┴ └───────┘ ┴ ┴ └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴
doc └──┘ └────┘
382 mk s (x - y) = mk s x - mk s y :=
id └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
src └┘ ┴ ┴ └┘ ┴ └┘
typ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
383 ext $ λ i, by simp only [sub_apply, mk_apply]; split_ifs; [refl, rw sub_zero]
id └─┘ ┴ └───────┘ └──────┘ ┴ └──────┘
src └─┘ └─────────┘└───────┘└┘└──────┘┴ └───────┘ ┴└──┘ └─┘└──────┘
typ └─┘ ┴ └─────────┘└───────┘└┘└──────┘┴ └───────┘ ┴└──┘ └─┘└──────┘
doc └─────────┘ └┘ ┴ └───────┘ └──┘ └─┘
txt └─────────┘ └┘ ┴ └───────┘ └──┘ └─┘
par └─────────┘ └┘ ┴ └───────┘ └──┘ └─┘
pid ┴└──┘└┘ └┘ ┴ ┴
st └─────────────────────────────────────────────────────┘└──────┘┴
384
385 instance [Π i, add_group (β i)] {s : finset ι} : is_add_group_hom (@mk ι β _ _ s) :=
id ┴ └───────┘ ┴ ┴ └────┘ ┴ └──────────────┘ └┘ ┴ ┴ ┴
src └───────┘ └────┘ └──────────────┘ └┘
typ ┴ └───────┘ ┴ ┴ └────┘ ┴ └──────────────┘ └┘ ┴ ┴ ┴
doc └────┘ └──────────────┘
386 { map_add := λ _ _, mk_add }
id ┴ ┴ └────┘
src └────┘
typ ┴ ┴ └────┘
387
388 section
389 local attribute [instance] to_module
id └───────┘
src └───────┘
typ └───────┘
390 variables (γ : Type w) [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)]
id └──┘ ┴ └────────────┘ ┴ ┴ └────┘ ┴
src └──┘ └────────────┘ └────┘
typ └──┘ ┴ └────────────┘ ┴ ┴ └────┘ ┴
doc └────┘
391 include γ
392 @[simp] lemma mk_smul {s : finset ι} {c : γ} (x : Π i : (↑s : set ι), β i.1) :
id └────┘ ┴ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴
src └────┘ ┴ └─┘ ┴
typ └────┘ ┴ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴
doc └──┘ └────┘
393 mk s (c • x) = c • mk s x :=
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └┘ ┴ ┴ ┴ └┘
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
394 ext $ λ i, by simp only [smul_apply, mk_apply]; split_ifs; [refl, rw smul_zero]
id └─┘ ┴ └────────┘ └──────┘ ┴ └───────┘
src └─┘ └─────────┘└────────┘└┘└──────┘┴ └───────┘ ┴└──┘ └─┘└───────┘
typ └─┘ ┴ └─────────┘└────────┘└┘└──────┘┴ └───────┘ ┴└──┘ └─┘└───────┘
doc └─────────┘ └┘ ┴ └───────┘ └──┘ └─┘
txt └─────────┘ └┘ ┴ └───────┘ └──┘ └─┘
par └─────────┘ └┘ ┴ └───────┘ └──┘ └─┘
pid ┴└──┘└┘ └┘ ┴ ┴
st └──────────────────────────────────────────────────────┘└───────┘┴
395
396 @[simp] lemma single_smul {i : ι} {c : γ} {x : β i} :
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
doc └──┘
397 single i (c • x) = c • single i x :=
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
src └────┘ ┴ ┴ ┴ └────┘
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
398 ext $ λ i, by simp only [smul_apply, single_apply]; split_ifs; [cases h, rw smul_zero]; refl
id └─┘ ┴ └────────┘ └──────────┘ ┴ ┴ └───────┘
src └─┘ └─────────┘└────────┘└┘└──────────┘┴ └───────┘ ┴└────┘ └─┘└───────┘ └────
typ └─┘ ┴ └─────────┘└────────┘└┘└──────────┘┴ └───────┘ ┴└────┘┴ └─┘└───────┘ └────
doc └─────────┘ └┘ ┴ └───────┘ └────┘ └─┘ └────
txt └─────────┘ └┘ ┴ └───────┘ └────┘ └─┘ └────
par └─────────┘ └┘ ┴ └───────┘ └────┘ └─┘ └────
pid ┴└──┘└┘ └┘ ┴ ┴ ┴ └
st └─────────────────────────────────────────────────────────────┘└───────┘└───────
399
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
400 variable β
401 def lmk (s : finset ι) : (Π i : (↑s : set ι), β i.1) →ₗ[γ] Π₀ i, β i :=
id └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴ └─┘┴┴ └┘ ┴┴ ┴ ┴
src └────┘ ┴ └─┘ ┴ └─┘ ┴ └┘ ┴
typ └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴ └─┘┴┴ └┘ ┴┴ ┴ ┴
doc └────┘
402 ⟨mk s, λ _ _, mk_add, λ c x, by rw [mk_smul γ x]⟩
id └┘ ┴ ┴ ┴ └────┘ ┴ ┴ └─────┘ ┴ ┴
src └┘ └────┘ └──┘└─────┘┴ ┴ ┴
typ └┘ ┴ ┴ ┴ └────┘ ┴ ┴ └──┘└─────┘┴┴┴┴┴
doc └──┘ ┴ ┴ ┴
txt └──┘ ┴ ┴ ┴
par └──┘ ┴ ┴ ┴
pid └┘ ┴ ┴ ┴
st └──────────────┘┴
403
404 def lsingle (i) : β i →ₗ[γ] Π₀ i, β i :=
id ┴ ┴ └─┘┴┴ └┘ ┴┴ ┴ ┴
src └─┘ ┴ └┘ ┴
typ ┴ ┴ └─┘┴┴ └┘ ┴┴ ┴ ┴
405 ⟨single i, λ _ _, single_add, λ _ _, single_smul _⟩
id └────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ └─────────┘
src └────┘ └────────┘ └─────────┘
typ └────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ └─────────┘
406 variable {β}
407
408 @[simp] lemma lmk_apply {s : finset ι} {x} : lmk β γ s x = mk s x := rfl
id └────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘
src └────┘ └─┘ ┴ └┘ └─┘
typ └────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └─┘
doc └──┘ └────┘
409
410 @[simp] lemma lsingle_apply {i : ι} {x : β i} : lsingle β γ i x = single i x := rfl
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘
src └─────┘ ┴ └────┘ └─┘
typ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘
doc └──┘
411 end
412
413 section support_basic
414
415 variables [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))]
id ┴ └──────┘ ┴ ┴ └────────────┘ └┘ ┴
src └──────┘ └────────────┘ └┘
typ ┴ └──────┘ ┴ ┴ └────────────┘ └┘ ┴
416
417 def support (f : Π₀ i, β i) : finset ι :=
id └┘ ┴┴ ┴ ┴ └────┘ ┴
src └┘ ┴ └────┘
typ └┘ ┴┴ ┴ ┴ └────┘ ┴
doc └────┘
418 quotient.lift_on f (λ x, x.2.to_finset.filter $ λ i, x.1 i ≠ 0) $
id └──────────────┘ ┴ ┴ ┴┴ └───────┘ └────┘ ┴ ┴┴ ┴ ┴
src └──────────────┘ ┴ └───────┘ └────┘ ┴ ┴
typ └──────────────┘ ┴ ┴ ┴┴ └───────┘ └────┘ ┴ ┴┴ ┴ ┴
doc └───────┘ └────┘
419 begin
st └─────
420 intros x y Hxy,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───────────────┘└─
421 ext i, split,
src └───┘ └───┘
typ └───┘ └───┘
doc └───┘ └───┘
txt └───┘ └───┘
par └───┘ └───┘
pid └┘
st ──────┘└─────┘└─
422 { intro H,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ───┘└─────┘└─
423 rcases finset.mem_filter.1 H with ⟨h1, h2⟩,
id └───────────────┘ ┴
src └─────┘└───────────────┘└─┘ └────────────┘
typ └─────┘└───────────────┘└─┘┴└────────────┘
doc └─────┘ └─┘ └────────────┘
txt └─────┘ └─┘ └────────────┘
par └─────┘ └─┘ └────────────┘
pid ┴ └─┘ └────────────┘
st ─────────────────────────────────────────────┘└─
424 rw Hxy i at h2,
id └─┘ ┴
src └─┘ ┴ └────┘
typ └─┘└─┘┴┴└────┘
doc └─┘ ┴ └────┘
txt └─┘ ┴ └────┘
par └─┘ ┴ └────┘
pid ┴ ┴ └────┘
st ─────────────────┘└─
425 exact finset.mem_filter.2 ⟨multiset.mem_to_finset.2 $ (y.3 i).resolve_right h2, h2⟩ },
id └───────────────┘ └────────────────────┘ ┴ ┴ └┘
src └────┘└───────────────┘└─┘ └────────────────────┘└─┘ ┴ └─┘ └──────────────┘ └┘ └┘
typ └────┘└───────────────┘└─┘ └────────────────────┘└─┘ ┴ ┴└─┘┴└──────────────┘ └┘└┘└┘
doc └────┘ └─┘ └─┘ ┴ └─┘ └──────────────┘ └┘ └┘
txt └────┘ └─┘ └─┘ ┴ └─┘ └──────────────┘ └┘ └┘
par └────┘ └─┘ └─┘ ┴ └─┘ └──────────────┘ └┘ └┘
pid ┴ └─┘ └─┘ ┴ └─┘ └──────────────┘ └┘ ┴┴
st ───────────────────────────────────────────────────────────────────────────────────────┘└┘└
426 { intro H,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ──────────┘└─
427 rcases finset.mem_filter.1 H with ⟨h1, h2⟩,
id └───────────────┘ ┴
src └─────┘└───────────────┘└─┘ └────────────┘
typ └─────┘└───────────────┘└─┘┴└────────────┘
doc └─────┘ └─┘ └────────────┘
txt └─────┘ └─┘ └────────────┘
par └─────┘ └─┘ └────────────┘
pid ┴ └─┘ └────────────┘
st ─────────────────────────────────────────────┘└─
428 rw ← Hxy i at h2,
id └─┘ ┴
src └───┘ ┴ └────┘
typ └───┘└─┘┴┴└────┘
doc └───┘ ┴ └────┘
txt └───┘ ┴ └────┘
par └───┘ ┴ └────┘
pid └─┘ ┴ └────┘
st ───────────────────┘└─
429 exact finset.mem_filter.2 ⟨multiset.mem_to_finset.2 $ (x.3 i).resolve_right h2, h2⟩ },
id └───────────────┘ └────────────────────┘ ┴ ┴ └┘
src └────┘└───────────────┘└─┘ └────────────────────┘└─┘ ┴ └─┘ └──────────────┘ └┘ └┘
typ └────┘└───────────────┘└─┘ └────────────────────┘└─┘ ┴ ┴└─┘┴└──────────────┘ └┘└┘└┘
doc └────┘ └─┘ └─┘ ┴ └─┘ └──────────────┘ └┘ └┘
txt └────┘ └─┘ └─┘ ┴ └─┘ └──────────────┘ └┘ └┘
par └────┘ └─┘ └─┘ ┴ └─┘ └──────────────┘ └┘ └┘
pid ┴ └─┘ └─┘ ┴ └─┘ └──────────────┘ └┘ ┴┴
st ───────────────────────────────────────────────────────────────────────────────────────┘└──
430 end
st ──┘
431
432 @[simp] theorem support_mk_subset {s : finset ι} {x : Π i : (↑s : set ι), β i.1} : (mk s x).support ⊆ s :=
id └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴ └┘ ┴ ┴ └─────┘ ┴ ┴
src └────┘ ┴ └─┘ ┴ └┘ └─────┘ ┴
typ └────┘ ┴ ┴┴┴ └─┘ ┴ ┴ ┴┴ └┘ ┴ ┴ └─────┘ ┴ ┴
doc └──┘ └────┘
433 λ i H, multiset.mem_to_finset.1 (finset.mem_filter.1 H).1
id ┴ ┴ └────────────────────┘┴ └───────────────┘┴ ┴ ┴
src └────────────────────┘┴ └───────────────┘┴ ┴
typ ┴ ┴ └────────────────────┘┴ └───────────────┘┴ ┴ ┴
434
435 @[simp] theorem mem_support_to_fun (f : Π₀ i, β i) (i) : i ∈ f.support ↔ f i ≠ 0 :=
id └┘ ┴┴ ┴ ┴ ┴ ┴ ┴└──────┘ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ └──────┘ ┴ ┴
typ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴└──────┘ ┴ ┴ ┴ ┴
doc └──┘
436 begin
st └─────
437 refine quotient.induction_on f (λ x, _),
id └───────────────────┘ ┴
src └─────┘└───────────────────┘┴ ┴ └────┘
typ └─────┘└───────────────────┘┴┴┴ └────┘
doc └─────┘ ┴ ┴ └────┘
txt └─────┘ ┴ ┴ └────┘
par └─────┘ ┴ ┴ └────┘
pid ┴ ┴ ┴ └────┘
st ────────────────────────────────────────┘└─
438 dsimp only [support, quotient.lift_on_beta],
id └─────┘ └───────────────────┘
src └──────────┘└─────┘└┘└───────────────────┘┴
typ └──────────┘└─────┘└┘└───────────────────┘┴
doc └──────────┘ └┘ ┴
txt └──────────┘ └┘ ┴
par └──────────┘ └┘ ┴
pid └───┘└┘ └┘ ┴
st ────────────────────────────────────────────┘└─
439 rw [finset.mem_filter, multiset.mem_to_finset],
id └───────────────┘ └────────────────────┘
src └──┘└───────────────┘└┘└────────────────────┘┴
typ └──┘└───────────────┘└┘└────────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────────┘└──────────────────────┘└──
440 exact and_iff_right_of_imp (x.3 i).resolve_right
id └──────────────────┘ ┴ ┴
src └────┘└──────────────────┘┴ └─┘ └──────────────┘
typ └────┘└──────────────────┘┴ ┴└─┘┴└──────────────┘
doc └────┘ ┴ └─┘ └──────────────┘
txt └────┘ ┴ └─┘ └──────────────┘
par └────┘ ┴ └─┘ └──────────────┘
pid ┴ ┴ └─┘ └────────────┘└┘
st ──────────────────────────────────────────────────┘
441 end
st └─┘
442
443 theorem eq_mk_support (f : Π₀ i, β i) : f = mk f.support (λ i, f i.1) :=
id └┘ ┴┴ ┴ ┴ ┴ ┴ └┘ ┴└──────┘ ┴ ┴ ┴┴
src └┘ ┴ ┴ └┘ └──────┘ ┴
typ └┘ ┴┴ ┴ ┴ ┴ ┴ └┘ ┴└──────┘ ┴ ┴ ┴┴
444 by ext i; by_cases h : f i = 0; try {simp at h}; simp [h]
id ┴ ┴ ┴ ┴
src └───┘ └───────┘ └─┘ ┴ ┴┴└┘ └───┘└───────┘┴ └────┘ └─
typ └───┘ └───────┘ └─┘┴┴┴┴┴└┘ └───┘└───────┘┴ └────┘┴└─
doc └───┘ └───────┘ └─┘ ┴ ┴ └┘ └───┘└───────┘┴ └────┘ └─
txt └───┘ └───────┘ └─┘ ┴ ┴ └┘ └───┘└───────┘┴ └────┘ └─
par └───┘ └───────┘ └─┘ ┴ ┴ └┘ └───┘└───────┘┴ └────┘ └─
pid └┘ ┴ └─┘ ┴ ┴ ┴┴ └──────────┘ ┴┴ ┴└
st └─────────────────────────────────┘└───────┘└┘└─────────
445
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
446 @[simp] lemma support_zero : (0 : Π₀ i, β i).support = ∅ := rfl
id └┘ ┴┴ ┴ ┴ └─────┘ ┴ ┴ └─┘
src └┘ ┴ └─────┘ ┴ ┴ └─┘
typ └┘ ┴┴ ┴ ┴ └─────┘ ┴ ┴ └─┘
doc └──┘
447
448 @[simp] lemma mem_support_iff (f : Π₀ i, β i) : ∀i:ι, i ∈ f.support ↔ f i ≠ 0 :=
id └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴└──────┘ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ └──────┘ ┴ ┴
typ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴└──────┘ ┴ ┴ ┴ ┴
doc └──┘
449 f.mem_support_to_fun
id ┴└─────────────────┘
src └─────────────────┘
typ ┴└─────────────────┘
450
451 @[simp] lemma support_eq_empty {f : Π₀ i, β i} : f.support = ∅ ↔ f = 0 :=
id └┘ ┴┴ ┴ ┴ ┴└──────┘ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └──────┘ ┴ ┴ ┴ ┴
typ └┘ ┴┴ ┴ ┴ ┴└──────┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
452 ⟨λ H, ext $ by simpa [finset.ext] using H, by simp {contextual:=tt}⟩
id ┴ └─┘ └────────┘ ┴ └┘
src └─┘ └─────┘└────────┘└──────┘ └───┘ └──────────┘└┘┴
typ ┴ └─┘ └─────┘└────────┘└──────┘┴ └───┘ └──────────┘└┘┴
doc └─────┘ └──────┘ └───┘ └──────────┘ ┴
txt └─────┘ └──────┘ └───┘ └──────────┘ ┴
par └─────┘ └──────┘ └───┘ └──────────┘ ┴
pid ┴┴ ┴┴└────┘ ┴ └──────────┘ ┴
st └─────────────────────────┘ └────────────────────┘
453
454 instance decidable_zero : decidable_pred (eq (0 : Π₀ i, β i)) :=
id └────────────┘ └┘ └┘ ┴┴ ┴ ┴
src └────────────┘ └┘ └┘ ┴
typ └────────────┘ └┘ └┘ ┴┴ ┴ ┴
455 λ f, decidable_of_iff _ $ support_eq_empty.trans eq_comm
id ┴ └──────────────┘ └──────────────┘└────┘ └─────┘
src └──────────────┘ └──────────────┘└────┘ └─────┘
typ ┴ └──────────────┘ └──────────────┘└────┘ └─────┘
456
457 lemma support_subset_iff {s : set ι} {f : Π₀ i, β i} :
id └─┘ ┴ └┘ ┴┴ ┴ ┴
src └─┘ └┘ ┴
typ └─┘ ┴ └┘ ┴┴ ┴ ┴
458 ↑f.support ⊆ s ↔ (∀i∉s, f i = 0) :=
id ┴┴└──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──────┘ ┴ ┴ ┴ ┴
typ ┴┴└──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
459 by simp [set.subset_def];
id └────────────┘
src └────┘└────────────┘┴
typ └────┘└────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └───────────────────────
460 exact forall_congr (assume i, @not_imp_comm _ _ (classical.dec _) (classical.dec _))
id └──────────┘ └──────────┘ └───────────┘
src └────┘└──────────┘┴ └──┘ └──────────┘└───┘ └──┘ └───────────┘└────
typ └────┘└──────────┘┴ └──┘ └──────────┘└───┘ └──┘ └───────────┘└────
doc └────┘ ┴ └──┘ └───┘ └──┘ └────
txt └────┘ ┴ └──┘ └───┘ └──┘ └────
par └────┘ ┴ └──┘ └───┘ └──┘ └────
pid ┴ ┴ └──┘ └───┘ └──┘ └──┘└
st ────────────────────────────────────────────────────────────────────────────────────────
461
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
462 lemma support_single_ne_zero {i : ι} {b : β i} (hb : b ≠ 0) : (single i b).support = {i} :=
id ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─────┘ ┴ ┴┴
src ┴ └────┘ └─────┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ └─────┘ ┴ ┴┴
463 begin
st └─────
464 ext j, by_cases h : i = j,
id ┴ ┴ ┴
src └───┘ └───────┘ └─┘ ┴┴┴
typ └───┘ └───────┘ └─┘┴┴┴┴┴
doc └───┘ └───────┘ └─┘ ┴ ┴
txt └───┘ └───────┘ └─┘ ┴ ┴
par └───┘ └───────┘ └─┘ ┴ ┴
pid └┘ ┴ └─┘ ┴ ┴
st ──────┘└──────────────────┘└─
465 { subst h, simp [hb] },
id ┴ └┘
src └────┘ └────┘ └┘
typ └────┘┴ └────┘└┘└┘
doc └────┘ └────┘ └┘
txt └────┘ └────┘ └┘
par └────┘ └────┘ └┘
pid ┴ ┴┴ ┴┴
st ───┘└─────┘└──────────┘└┘└
466 simp [ne.symm h, h]
id └─────┘ ┴ ┴
src └────┘└─────┘┴ └┘ └┘
typ └────┘└─────┘┴┴└┘┴└┘
doc └────┘ ┴ └┘ └┘
txt └────┘ ┴ └┘ └┘
par └────┘ ┴ └┘ └┘
pid ┴┴ ┴ └┘ ┴┴
st ─────────────────────┘
467 end
st └─┘
468
469 lemma support_single_subset {i : ι} {b : β i} : (single i b).support ⊆ {i} :=
id ┴ ┴ ┴ └────┘ ┴ ┴ └─────┘ ┴ ┴┴
src └────┘ └─────┘ ┴ ┴
typ ┴ ┴ ┴ └────┘ ┴ ┴ └─────┘ ┴ ┴┴
470 support_mk_subset
id └───────────────┘
src └───────────────┘
typ └───────────────┘
471
472 section map_range_and_zip_with
473
474 variables {β₁ : ι → Type v₁} {β₂ : ι → Type v₂}
475 variables [Π i, has_zero (β₁ i)] [Π i, has_zero (β₂ i)]
id ┴ └──────┘ ┴ ┴ └──────┘ ┴
src └──────┘ └──────┘
typ ┴ └──────┘ ┴ ┴ └──────┘ ┴
476 variables [Π i, decidable_pred (eq (0 : β₁ i))] [Π i, decidable_pred (eq (0 : β₂ i))]
id ┴ └────────────┘ └┘ ┴ ┴ └────────────┘ └┘ ┴
src └────────────┘ └┘ └────────────┘ └┘
typ ┴ └────────────┘ └┘ ┴ ┴ └────────────┘ └┘ ┴
477
478 lemma map_range_def {f : Π i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} :
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴
src ┴ └┘ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴
479 map_range f hf g = mk g.support (λ i, f i.1 (g i.1)) :=
id └───────┘ ┴ └┘ ┴ ┴ └┘ ┴└──────┘ ┴ ┴ ┴┴ ┴ ┴┴
src └───────┘ ┴ └┘ └──────┘ ┴ ┴
typ └───────┘ ┴ └┘ ┴ ┴ └┘ ┴└──────┘ ┴ ┴ ┴┴ ┴ ┴┴
doc └───────┘
480 begin
st └─────
481 ext i,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
482 by_cases h : g i = 0,
id ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴┴└┘
typ └───────┘ └─┘┴┴┴┴┴└┘
doc └───────┘ └─┘ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴┴
st ─────────────────────┘└─
483 { simp [h, hf] },
id ┴ └┘
src └────┘ └┘ └┘
typ └────┘┴└┘└┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ───┘└───────────┘└┘└
484 { simp at h, simp [h, hf] }
id ┴ └┘
src └───────┘ └────┘ └┘ └┘
typ └───────┘ └────┘┴└┘└┘└┘
doc └───────┘ └────┘ └┘ └┘
txt └───────┘ └────┘ └┘ └┘
par └───────┘ └────┘ └┘ └┘
pid ┴└──┘ ┴┴ └┘ ┴┴
st ────────────┘└─────────────┘└─
485 end
st ──┘
486
487 lemma support_map_range {f : Π i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} :
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴
src ┴ └┘ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴
488 (map_range f hf g).support ⊆ g.support :=
id └───────┘ ┴ └┘ ┴ └─────┘ ┴ ┴└──────┘
src └───────┘ └─────┘ ┴ └──────┘
typ └───────┘ ┴ └┘ ┴ └─────┘ ┴ ┴└──────┘
doc └───────┘
489 by simp [map_range_def]
id └───────────┘
src └────┘└───────────┘└─
typ └────┘└───────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └─────────────────────
490
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
491 @[simp] lemma map_range_single {f : Π i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {i : ι} {b : β₁ i} :
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └──┘
492 map_range f hf (single i b) = single i (f i b) :=
id └───────┘ ┴ └┘ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
src └───────┘ └────┘ ┴ └────┘
typ └───────┘ ┴ └┘ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
doc └───────┘
493 dfinsupp.ext $ λ i', by by_cases i = i'; [{subst i', simp}, simp [h, hf]]
id └──────────┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘
src └──────────┘ └───────┘ ┴┴┴ ┴ └────┘ └──┘ └────┘ └┘ ┴
typ └──────────┘ └┘ └───────┘┴┴┴┴└┘ ┴ └────┘└┘ └──┘ └────┘┴└┘└┘┴
doc └───────┘ ┴ ┴ └────┘ └──┘ └────┘ └┘ ┴
txt └───────┘ ┴ ┴ └────┘ └──┘ └────┘ └┘ ┴
par └───────┘ ┴ ┴ └────┘ └──┘ └────┘ └┘ ┴
pid ┴ ┴ ┴ ┴ ┴┴ └┘ ┴
st └─────────────────┘└───────┘└────┘└┘└────────────┘
494
495 lemma zip_with_def {f : Π i, β₁ i → β₂ i → β i} {hf : ∀ i, f i 0 0 = 0} {g₁ : Π₀ i, β₁ i} {g₂ : Π₀ i, β₂ i} :
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ └┘ ┴┴ └┘ ┴
src ┴ └┘ ┴ └┘ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ └┘ ┴┴ └┘ ┴
496 zip_with f hf g₁ g₂ = mk (g₁.support ∪ g₂.support) (λ i, f i.1 (g₁ i.1) (g₂ i.1)) :=
id └──────┘ ┴ └┘ └┘ └┘ ┴ └┘ └┘└──────┘ ┴ └┘└──────┘ ┴ ┴ ┴┴ └┘ ┴┴ └┘ ┴┴
src └──────┘ ┴ └┘ └──────┘ ┴ └──────┘ ┴ ┴ ┴
typ └──────┘ ┴ └┘ └┘ └┘ ┴ └┘ └┘└──────┘ ┴ └┘└──────┘ ┴ ┴ ┴┴ └┘ ┴┴ └┘ ┴┴
497 begin
st └─────
498 ext i,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
499 by_cases h1 : g₁ i = 0; by_cases h2 : g₂ i = 0;
id └┘ ┴ ┴ └┘ ┴
src └───────┘ └─┘ ┴ ┴┴└┘ └───────┘ └─┘ ┴ ┴ └┘
typ └───────┘ └─┘└┘┴┴┴┴└┘ └───────┘ └─┘└┘┴┴┴ └┘
doc └───────┘ └─┘ ┴ ┴ └┘ └───────┘ └─┘ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ └┘ └───────┘ └─┘ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ └┘ └───────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴┴ ┴ └─┘ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────
500 try {simp at h1 h2}; simp [h1, h2, hf]
id └┘ └┘ └┘
src └───┘└───────────┘┴ └────┘ └┘ └┘ └┘
typ └───┘└───────────┘┴ └────┘└┘└┘└┘└┘└┘└┘
doc └───┘└───────────┘┴ └────┘ └┘ └┘ └┘
txt └───┘└───────────┘┴ └────┘ └┘ └┘ └┘
par └───┘└───────────┘┴ └────┘ └┘ └┘ └┘
pid └──────────────┘ ┴┴ └┘ └┘ ┴┴
st ──────┘└───────────┘└┘└─────────────────┘
501 end
st └─┘
502
503 lemma support_zip_with {f : Π i, β₁ i → β₂ i → β i} {hf : ∀ i, f i 0 0 = 0} {g₁ : Π₀ i, β₁ i} {g₂ : Π₀ i, β₂ i} :
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ └┘ ┴┴ └┘ ┴
src ┴ └┘ ┴ └┘ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ └┘ ┴┴ └┘ ┴
504 (zip_with f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support :=
id └──────┘ ┴ └┘ └┘ └┘ └─────┘ ┴ └┘└──────┘ ┴ └┘└──────┘
src └──────┘ └─────┘ ┴ └──────┘ ┴ └──────┘
typ └──────┘ ┴ └┘ └┘ └┘ └─────┘ ┴ └┘└──────┘ ┴ └┘└──────┘
505 by simp [zip_with_def]
id └──────────┘
src └────┘└──────────┘└─
typ └────┘└──────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────────
506
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
507 end map_range_and_zip_with
508
509 lemma erase_def (i : ι) (f : Π₀ i, β i) :
id ┴ └┘ ┴┴ ┴ ┴
src └┘ ┴
typ ┴ └┘ ┴┴ ┴ ┴
510 f.erase i = mk (f.support.erase i) (λ j, f j.1) :=
id ┴└────┘ ┴ ┴ └┘ ┴└──────┘└────┘ ┴ ┴ ┴ ┴┴
src └────┘ ┴ └┘ └──────┘└────┘ ┴
typ ┴└────┘ ┴ ┴ └┘ ┴└──────┘└────┘ ┴ ┴ ┴ ┴┴
doc └────┘
511 begin
st └─────
512 ext j,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
513 by_cases h1 : j = i; by_cases h2 : f j = 0;
id ┴ ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴┴┴ └───────┘ └─┘ ┴ ┴ └┘
typ └───────┘ └─┘┴┴┴┴┴ └───────┘ └─┘┴┴┴┴ └┘
doc └───────┘ └─┘ ┴ ┴ └───────┘ └─┘ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ └───────┘ └─┘ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ └───────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴
st ──────────────────────────────────────────────
514 try {simp at h2}; simp [h1, h2]
id └┘ └┘
src └───┘└────────┘┴ └────┘ └┘ └┘
typ └───┘└────────┘┴ └────┘└┘└┘└┘└┘
doc └───┘└────────┘┴ └────┘ └┘ └┘
txt └───┘└────────┘┴ └────┘ └┘ └┘
par └───┘└────────┘┴ └────┘ └┘ └┘
pid └───────────┘ ┴┴ └┘ ┴┴
st ──────┘└────────┘└┘└─────────────┘
515 end
st └─┘
516
517 @[simp] lemma support_erase (i : ι) (f : Π₀ i, β i) :
id ┴ └┘ ┴┴ ┴ ┴
src └┘ ┴
typ ┴ └┘ ┴┴ ┴ ┴
doc └──┘
518 (f.erase i).support = f.support.erase i :=
id ┴└────┘ ┴ └─────┘ ┴ ┴└──────┘└────┘ ┴
src └────┘ └─────┘ ┴ └──────┘└────┘
typ ┴└────┘ ┴ └─────┘ ┴ ┴└──────┘└────┘ ┴
doc └────┘
519 begin
st └─────
520 ext j,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
521 by_cases h1 : j = i; by_cases h2 : f j = 0;
id ┴ ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴┴┴ └───────┘ └─┘ ┴ ┴ └┘
typ └───────┘ └─┘┴┴┴┴┴ └───────┘ └─┘┴┴┴┴ └┘
doc └───────┘ └─┘ ┴ ┴ └───────┘ └─┘ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ └───────┘ └─┘ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ └───────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴┴
st ──────────────────────────────────────────────
522 try {simp at h2}; simp [h1, h2]
id └┘ └┘
src └───┘└────────┘┴ └────┘ └┘ └┘
typ └───┘└────────┘┴ └────┘└┘└┘└┘└┘
doc └───┘└────────┘┴ └────┘ └┘ └┘
txt └───┘└────────┘┴ └────┘ └┘ └┘
par └───┘└────────┘┴ └────┘ └┘ └┘
pid └───────────┘ ┴┴ └┘ ┴┴
st ──────┘└────────┘└┘└─────────────┘
523 end
st └─┘
524
525 section filter_and_subtype_domain
526
527 variables {p : ι → Prop} [decidable_pred p]
id └────────────┘
src └────────────┘
typ └────────────┘
528
529 lemma filter_def (f : Π₀ i, β i) :
id └┘ ┴┴ ┴ ┴
src └┘ ┴
typ └┘ ┴┴ ┴ ┴
530 f.filter p = mk (f.support.filter p) (λ i, f i.1) :=
id ┴└─────┘ ┴ ┴ └┘ ┴└──────┘└─────┘ ┴ ┴ ┴ ┴┴
src └─────┘ ┴ └┘ └──────┘└─────┘ ┴
typ ┴└─────┘ ┴ ┴ └┘ ┴└──────┘└─────┘ ┴ ┴ ┴ ┴┴
doc └─────┘ └─────┘
531 by ext i; by_cases h1 : p i; by_cases h2 : f i = 0;
id ┴ ┴ ┴ ┴ ┴
src └───┘ └───────┘ └─┘ ┴ └───────┘ └─┘ ┴ ┴┴└┘
typ └───┘ └───────┘ └─┘┴┴┴ └───────┘ └─┘┴┴┴┴┴└┘
doc └───┘ └───────┘ └─┘ ┴ └───────┘ └─┘ ┴ ┴ └┘
txt └───┘ └───────┘ └─┘ ┴ └───────┘ └─┘ ┴ ┴ └┘
par └───┘ └───────┘ └─┘ ┴ └───────┘ └─┘ ┴ ┴ └┘
pid └┘ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴┴
st └─────────────────────────────────────────────────
532 try {simp at h2}; simp [h1, h2]
id └┘ └┘
src └───┘└────────┘┴ └────┘ └┘ └─
typ └───┘└────────┘┴ └────┘└┘└┘└┘└─
doc └───┘└────────┘┴ └────┘ └┘ └─
txt └───┘└────────┘┴ └────┘ └┘ └─
par └───┘└────────┘┴ └────┘ └┘ └─
pid └───────────┘ ┴┴ └┘ ┴└
st ────┘└────────┘└┘└──────────────
533
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
534 @[simp] lemma support_filter (f : Π₀ i, β i) :
id └┘ ┴┴ ┴ ┴
src └┘ ┴
typ └┘ ┴┴ ┴ ┴
doc └──┘
535 (f.filter p).support = f.support.filter p :=
id ┴└─────┘ ┴ └─────┘ ┴ ┴└──────┘└─────┘ ┴
src └─────┘ └─────┘ ┴ └──────┘└─────┘
typ ┴└─────┘ ┴ └─────┘ ┴ ┴└──────┘└─────┘ ┴
doc └─────┘ └─────┘
536 by ext i; by_cases h : p i; simp [h]
id ┴ ┴ ┴
src └───┘ └───────┘ └─┘ ┴ └────┘ └─
typ └───┘ └───────┘ └─┘┴┴┴ └────┘┴└─
doc └───┘ └───────┘ └─┘ ┴ └────┘ └─
txt └───┘ └───────┘ └─┘ ┴ └────┘ └─
par └───┘ └───────┘ └─┘ ┴ └────┘ └─
pid └┘ ┴ └─┘ ┴ ┴┴ ┴└
st └──────────────────────────────────
537
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
538 lemma subtype_domain_def (f : Π₀ i, β i) :
id └┘ ┴┴ ┴ ┴
src └┘ ┴
typ └┘ ┴┴ ┴ ┴
539 f.subtype_domain p = mk (f.support.subtype p) (λ i, f i.1) :=
id ┴└─────────────┘ ┴ ┴ └┘ ┴└──────┘└──────┘ ┴ ┴ ┴ ┴┴
src └─────────────┘ ┴ └┘ └──────┘└──────┘ ┴
typ ┴└─────────────┘ ┴ ┴ └┘ ┴└──────┘└──────┘ ┴ ┴ ┴ ┴┴
doc └─────────────┘
540 by ext i; cases i with i hi;
id ┴
src └───┘ └────┘ └────────┘
typ └───┘ └────┘┴└────────┘
doc └───┘ └────┘ └────────┘
txt └───┘ └────┘ └────────┘
par └───┘ └────┘ └────────┘
pid └┘ ┴ └────────┘
st └──────────────────────────
541 by_cases h1 : p i; by_cases h2 : f i = 0;
id ┴ ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴ └───────┘ └─┘ ┴ ┴┴└┘
typ └───────┘ └─┘┴┴┴ └───────┘ └─┘┴┴┴┴┴└┘
doc └───────┘ └─┘ ┴ └───────┘ └─┘ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ └───────┘ └─┘ ┴ ┴ └┘
par └───────┘ └─┘ ┴ └───────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴┴
st ──────────────────────────────────────────
542 try {simp at h2}; dsimp; simp [h1, h2]
id └┘ └┘
src └───┘└────────┘┴ └───┘ └────┘ └┘ └─
typ └───┘└────────┘┴ └───┘ └────┘└┘└┘└┘└─
doc └───┘└────────┘┴ └───┘ └────┘ └┘ └─
txt └───┘└────────┘┴ └───┘ └────┘ └┘ └─
par └───┘└────────┘┴ └───┘ └────┘ └┘ └─
pid └───────────┘ ┴┴ └┘ ┴└
st ────┘└────────┘└┘└─────────────────────
543
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
544 @[simp] lemma support_subtype_domain {f : Π₀ i, β i} :
id └┘ ┴┴ ┴ ┴
src └┘ ┴
typ └┘ ┴┴ ┴ ┴
doc └──┘
545 (subtype_domain p f).support = f.support.subtype p :=
id └────────────┘ ┴ ┴ └─────┘ ┴ ┴└──────┘└──────┘ ┴
src └────────────┘ └─────┘ ┴ └──────┘└──────┘
typ └────────────┘ ┴ ┴ └─────┘ ┴ ┴└──────┘└──────┘ ┴
doc └────────────┘
546 by ext i; cases i with i hi;
id ┴
src └───┘ └────┘ └────────┘
typ └───┘ └────┘┴└────────┘
doc └───┘ └────┘ └────────┘
txt └───┘ └────┘ └────────┘
par └───┘ └────┘ └────────┘
pid └┘ ┴ └────────┘
st └──────────────────────────
547 by_cases h1 : p i; by_cases h2 : f i = 0;
id ┴ ┴ ┴ ┴ ┴
src └───────┘ └─┘ ┴ └───────┘ └─┘ ┴ ┴┴└┘
typ └───────┘ └─┘┴┴┴ └───────┘ └─┘┴┴┴┴┴└┘
doc └───────┘ └─┘ ┴ └───────┘ └─┘ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ └───────┘ └─┘ ┴ ┴ └┘
par └───────┘ └─┘ ┴ └───────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴┴
st ──────────────────────────────────────────
548 try {simp at h2}; dsimp; simp [h1, h2]
id └┘ └┘
src └───┘└────────┘┴ └───┘ └────┘ └┘ └─
typ └───┘└────────┘┴ └───┘ └────┘└┘└┘└┘└─
doc └───┘└────────┘┴ └───┘ └────┘ └┘ └─
txt └───┘└────────┘┴ └───┘ └────┘ └┘ └─
par └───┘└────────┘┴ └───┘ └────┘ └┘ └─
pid └───────────┘ ┴┴ └┘ ┴└
st ────┘└────────┘└┘└─────────────────────
549
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
550 end filter_and_subtype_domain
551
552 end support_basic
553
554 lemma support_add [Π i, add_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))] {g₁ g₂ : Π₀ i, β i} :
id ┴ └────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └┘ ┴┴ ┴ ┴
src └────────┘ └────────────┘ └┘ └┘ ┴
typ ┴ └────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └┘ ┴┴ ┴ ┴
555 (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support :=
id └┘ ┴ └┘ └─────┘ ┴ └┘└──────┘ ┴ └┘└──────┘
src ┴ └─────┘ ┴ └──────┘ ┴ └──────┘
typ └┘ ┴ └┘ └─────┘ ┴ └┘└──────┘ ┴ └┘└──────┘
556 support_zip_with
id └──────────────┘
src └──────────────┘
typ └──────────────┘
557
558 @[simp] lemma support_neg [Π i, add_group (β i)] [Π i, decidable_pred (eq (0 : β i))] {f : Π₀ i, β i} :
id ┴ └───────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └┘ ┴┴ ┴ ┴
src └───────┘ └────────────┘ └┘ └┘ ┴
typ ┴ └───────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └┘ ┴┴ ┴ ┴
doc └──┘
559 support (-f) = support f :=
id └─────┘ ┴┴ ┴ └─────┘ ┴
src └─────┘ ┴ ┴ └─────┘
typ └─────┘ ┴┴ ┴ └─────┘ ┴
560 by ext i; simp
src └───┘ └────
typ └───┘ └────
doc └───┘ └────
txt └───┘ └────
par └───┘ └────
pid └┘ └
st └────────────
561
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
562 local attribute [instance] dfinsupp.to_module
id └────────────────┘
src └────────────────┘
typ └────────────────┘
563
564 lemma support_smul {γ : Type w} [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)]
id └──┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └──┘ └────────────┘ └────┘
typ └──┘ ┴ ┴ └────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └────┘
565 [Π (i : ι), decidable_pred (eq (0 : β i))]
id ┴ └────────────┘ └┘ ┴ ┴
src └────────────┘ └┘
typ ┴ └────────────┘ └┘ ┴ ┴
566 {b : γ} {v : Π₀ i, β i} : (b • v).support ⊆ v.support :=
id ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──────┘
src └┘ ┴ ┴ └─────┘ ┴ └──────┘
typ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴└──────┘
567 λ x, by simp [dfinsupp.mem_support_iff, not_imp_not] {contextual := tt}
id ┴ └──────────────────────┘ └─────────┘ └┘
src └────┘└──────────────────────┘└┘└─────────┘└┘ └────────────┘└┘└─
typ ┴ └────┘└──────────────────────┘└┘└─────────┘└┘ └────────────┘└┘└─
doc └────┘ └┘ └┘ └────────────┘ └─
txt └────┘ └┘ └┘ └────────────┘ └─
par └────┘ └┘ └┘ └────────────┘ └─
pid ┴┴ └┘ ┴┴ └────────────┘ ┴└
st └────────────────────────────────────────────────────────────────
568
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
569 instance [decidable_eq ι] [Π i, has_zero (β i)] [Π i, decidable_eq (β i)] : decidable_eq (Π₀ i, β i) :=
id └──────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ └┘ ┴┴ ┴ ┴
src └──────────┘ └──────┘ └──────────┘ └──────────┘ └┘ ┴
typ └──────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────────┘ ┴ ┴ └──────────┘ └┘ ┴┴ ┴ ┴
570 assume f g, decidable_of_iff (f.support = g.support ∧ (∀i∈f.support, f i = g i))
id ┴ ┴ └──────────────┘ ┴└──────┘ ┴ ┴└──────┘ ┴ ┴ ┴└──────┘ ┴ ┴ ┴ ┴ ┴
src └──────────────┘ └──────┘ ┴ └──────┘ ┴ └──────┘ ┴
typ ┴ ┴ └──────────────┘ ┴└──────┘ ┴ ┴└──────┘ ┴ ┴ ┴└──────┘ ┴ ┴ ┴ ┴ ┴
571 ⟨assume ⟨h₁, h₂⟩, ext $ assume i,
id ┴ └┘ └─┘ ┴
src └─┘
typ ┴ └┘ └─┘ ┴
572 if h : i ∈ f.support then h₂ i h else
id └┘ ┴ ┴ ┴└──────┘ ┴ ┴
src └┘ ┴ └──────┘
typ └┘ ┴ ┴ ┴└──────┘ ┴ ┴
573 have hf : f i = 0, by rwa [f.mem_support_iff, not_not] at h,
id └──┘ ┴ ┴ ┴ └─────┘
src ┴ └───┘ └┘└─────┘└────┘
typ └──┘ ┴ ┴ ┴ └───┘└───────────────┘└┘└─────┘└────┘
doc └───┘ └┘ └────┘
txt └───┘ └┘ └────┘
par └───┘ └┘ └────┘
pid └┘ └┘ ┴└───┘
st └─────────────────────┘└───────┘┴└───┘
574 have hg : g i = 0, by rwa [h₁, g.mem_support_iff, not_not] at h,
id ┴ ┴ ┴ └┘ └─────┘
src ┴ └───┘ └┘ └┘└─────┘└────┘
typ ┴ ┴ ┴ └───┘└┘└┘└───────────────┘└┘└─────┘└────┘
doc └───┘ └┘ └┘ └────┘
txt └───┘ └┘ └┘ └────┘
par └───┘ └┘ └┘ └────┘
pid └┘ └┘ └┘ ┴└───┘
st └──────┘└─────────────────┘└───────┘┴└───┘
575 by rw [hf, hg],
id └┘ └┘
src └──┘ └┘ ┴
typ └──┘└┘└┘└┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └─────┘└──┘┴
576 by intro h; subst h; simp⟩
id ┴
src └─────┘ └────┘ └──┘
typ └─────┘ └────┘┴ └──┘
doc └─────┘ └────┘ └──┘
txt └─────┘ └────┘ └──┘
par └─────┘ └────┘ └──┘
pid └┘ ┴
st └─────────────────────┘
577
578 section prod_and_sum
579
580 variables {γ : Type w}
581
582 -- [to_additive sum] for dfinsupp.prod doesn't work, the equation lemmas are not generated
583 /-- `sum f g` is the sum of `g i (f i)` over the support of `f`. -/
584 def sum [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))] [add_comm_monoid γ]
id ┴ └──────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └─────────────┘ ┴
src └──────┘ └────────────┘ └┘ └─────────────┘
typ ┴ └──────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └─────────────┘ ┴
585 (f : Π₀ i, β i) (g : Π i, β i → γ) : γ :=
id └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴
typ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
586 f.support.sum (λi, g i (f i))
id ┴└──────┘└──┘ ┴ ┴ ┴ ┴ ┴
src └──────┘└──┘
typ ┴└──────┘└──┘ ┴ ┴ ┴ ┴ ┴
587
588 /-- `prod f g` is the product of `g i (f i)` over the support of `f`. -/
589 @[to_additive]
doc └─────────┘
590 def prod [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ]
id ┴ └──────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └─────────┘ ┴
src └──────┘ └────────────┘ └┘ └─────────┘
typ ┴ └──────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └─────────┘ ┴
591 (f : Π₀ i, β i) (g : Π i, β i → γ) : γ :=
id └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴
typ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
592 f.support.prod (λi, g i (f i))
id ┴└──────┘└───┘ ┴ ┴ ┴ ┴ ┴
src └──────┘└───┘
typ ┴└──────┘└───┘ ┴ ┴ ┴ ┴ ┴
doc └───┘
593
594 @[to_additive]
doc └─────────┘
595 lemma prod_map_range_index {β₁ : ι → Type v₁} {β₂ : ι → Type v₂}
id ┴ ┴
typ ┴ ┴
596 [Π i, has_zero (β₁ i)] [Π i, has_zero (β₂ i)]
id ┴ └──────┘ └┘ ┴ ┴ └──────┘ └┘ ┴
src └──────┘ └──────┘
typ ┴ └──────┘ └┘ ┴ ┴ └──────┘ └┘ ┴
597 [Π i, decidable_pred (eq (0 : β₁ i))] [Π i, decidable_pred (eq (0 : β₂ i))] [comm_monoid γ]
id ┴ └────────────┘ └┘ └┘ ┴ ┴ └────────────┘ └┘ └┘ ┴ └─────────┘ ┴
src └────────────┘ └┘ └────────────┘ └┘ └─────────┘
typ ┴ └────────────┘ └┘ └┘ ┴ ┴ └────────────┘ └┘ └┘ ┴ └─────────┘ ┴
598 {f : Π i, β₁ i → β₂ i} {hf : ∀ i, f i 0 = 0} {g : Π₀ i, β₁ i} {h : Π i, β₂ i → γ} (h0 : ∀i, h i 0 = 1) :
id ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ ┴ ┴
typ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
599 (map_range f hf g).prod h = g.prod (λi b, h i (f i b)) :=
id └───────┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ └──┘ ┴ └───┘
typ └───────┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └──┘ └───┘
600 begin
st └─────
601 rw [map_range_def],
id └───────────┘
src └──┘└───────────┘┴
typ └──┘└───────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ──────────────────┘└──
602 refine (finset.prod_subset support_mk_subset _).trans _,
id └────────────────┘ └───────────────┘
src └─────┘ └────────────────┘┴└───────────────┘└─────────┘
typ └─────┘ └────────────────┘┴└───────────────┘└─────────┘
doc └─────┘ ┴ └─────────┘
txt └─────┘ ┴ └─────────┘
par └─────┘ ┴ └─────────┘
pid ┴ ┴ └─────────┘
st ────────────────────────────────────────────────────────┘└─
603 { intros i h1 h2,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───┘└────────────┘└─
604 dsimp, simp [h1] at h2, dsimp at h2,
id └┘
src └───┘ └────┘ └─────┘ └─────────┘
typ └───┘ └────┘└┘└─────┘ └─────────┘
doc └───┘ └────┘ └─────┘ └─────────┘
txt └───┘ └────┘ └─────┘ └─────────┘
par └───┘ └────┘ └─────┘ └─────────┘
pid ┴┴ ┴┴└───┘ ┴└───┘
st ────────┘└───────────────┘└───────────┘└─
605 simp [h1, h2, h0] },
id └┘ └┘ └┘
src └────┘ └┘ └┘ └┘
typ └────┘└┘└┘└┘└┘└┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
st ─────────────────────┘└┘└
606 { refine finset.prod_congr rfl _,
id └───────────────┘ └─┘
src └─────┘└───────────────┘┴└─┘└┘
typ └─────┘└───────────────┘┴└─┘└┘
doc └─────┘ ┴ └┘
txt └─────┘ ┴ └┘
par └─────┘ ┴ └┘
pid ┴ ┴ └┘
st ─────────────────────────────────┘└─
607 intros i h1,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ──────────────┘└─
608 simp [h1] }
id └┘
src └────┘ └┘
typ └────┘└┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ─────────────┘└─
609 end
st ──┘
610
611 @[to_additive]
doc └─────────┘
612 lemma prod_zero_index [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ]
id ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └─────────┘ ┴
src └─────────────┘ └────────────┘ └┘ └─────────┘
typ ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └─────────┘ ┴
613 {h : Π i, β i → γ} : (0 : Π₀ i, β i).prod h = 1 :=
id ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ └──┘ ┴ ┴
src └┘ ┴ └──┘ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴ └──┘ ┴ ┴
doc └──┘
614 rfl
id └─┘
src └─┘
typ └─┘
615
616 @[to_additive]
doc └─────────┘
617 lemma prod_single_index [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ]
id ┴ └──────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └─────────┘ ┴
src └──────┘ └────────────┘ └┘ └─────────┘
typ ┴ └──────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └─────────┘ ┴
618 {i : ι} {b : β i} {h : Π i, β i → γ} (h_zero : h i 0 = 1) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
619 (single i b).prod h = h i b :=
id └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └────┘ └──┘ ┴
typ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
620 begin
st └─────
621 by_cases h : b = 0,
id ┴ ┴
src └───────┘ └─┘ ┴┴└┘
typ └───────┘ └─┘┴┴┴└┘
doc └───────┘ └─┘ ┴ └┘
txt └───────┘ └─┘ ┴ └┘
par └───────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ───────────────────┘└─
622 { simp [h, prod_zero_index, h_zero], refl },
id ┴ └─────────────┘ └────┘
src └────┘ └┘└─────────────┘└┘ ┴ └───┘
typ └────┘┴└┘└─────────────┘└┘└────┘┴ └───┘
doc └────┘ └┘ └┘ ┴ └───┘
txt └────┘ └┘ └┘ ┴ └───┘
par └────┘ └┘ └┘ ┴ └───┘
pid ┴┴ └┘ └┘ ┴ ┴
st ───┘└───────────────────────────────┘└─────┘└┘└
623 { simp [dfinsupp.prod, support_single_ne_zero h] }
id └───────────┘ └────────────────────┘ ┴
src └────┘└───────────┘└┘└────────────────────┘┴ └┘
typ └────┘└───────────┘└┘└────────────────────┘┴┴└┘
doc └────┘└───────────┘└┘ ┴ └┘
txt └────┘ └┘ ┴ └┘
par └────┘ └┘ ┴ └┘
pid ┴┴ └┘ ┴ ┴┴
st ──────────────────────────────────────────────────┘└─
624 end
st ──┘
625
626 @[to_additive]
doc └─────────┘
627 lemma prod_neg_index [Π i, add_group (β i)] [Π i, decidable_pred (eq (0 : β i))] [comm_monoid γ]
id ┴ └───────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └─────────┘ ┴
src └───────┘ └────────────┘ └┘ └─────────┘
typ ┴ └───────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴ └─────────┘ ┴
628 {g : Π₀ i, β i} {h : Π i, β i → γ} (h0 : ∀i, h i 0 = 1) :
id └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
629 (-g).prod h = g.prod (λi b, h i (- b)) :=
id ┴┴ └──┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ └───┘ ┴
typ ┴┴ └──┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └───┘
630 prod_map_range_index h0
id └──────────────────┘ └┘
src └──────────────────┘
typ └──────────────────┘ └┘
631
632 @[simp] lemma sum_apply {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ → Type v₁}
id └──────────┘ └┘ └┘
src └──────────┘
typ └──────────┘ └┘ └┘
doc └──┘
633 [Π i₁, has_zero (β₁ i₁)] [Π i, decidable_pred (eq (0 : β₁ i))]
id └┘ └──────┘ └┘ └┘ ┴ └────────────┘ └┘ └┘ ┴
src └──────┘ └────────────┘ └┘
typ └┘ └──────┘ └┘ └┘ ┴ └────────────┘ └┘ └┘ ┴
634 [Π i, add_comm_monoid (β i)]
id ┴ └─────────────┘ ┴ ┴
src └─────────────┘
typ ┴ └─────────────┘ ┴ ┴
635 {f : Π₀ i₁, β₁ i₁} {g : Π i₁, β₁ i₁ → Π₀ i, β i} {i₂ : ι} :
id └┘ └┘┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴┴ ┴ ┴ ┴
src └┘ ┴ └┘ ┴
typ └┘ └┘┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴┴ ┴ ┴ ┴
636 (f.sum g) i₂ = f.sum (λi₁ b, g i₁ b i₂) :=
id ┴└──┘ ┴ └┘ ┴ ┴└──┘ └┘ ┴ ┴ └┘ ┴ └┘
src └──┘ ┴ └──┘
typ ┴└──┘ ┴ └┘ ┴ ┴└──┘ └┘ ┴ ┴ └┘ ┴ └┘
doc └──┘ └──┘
637 (f.support.sum_hom (λf : Π₀ i, β i, f i₂)).symm
id ┴└──────┘└──────┘ └┘ ┴┴ ┴ ┴ ┴ └┘ └──┘
src └──────┘└──────┘ └┘ ┴ └──┘
typ ┴└──────┘└──────┘ └┘ ┴┴ ┴ ┴ ┴ └┘ └──┘
638
639 lemma support_sum {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ → Type v₁}
id └──────────┘ └┘ └┘
src └──────────┘
typ └──────────┘ └┘ └┘
640 [Π i₁, has_zero (β₁ i₁)] [Π i, decidable_pred (eq (0 : β₁ i))]
id └┘ └──────┘ └┘ └┘ ┴ └────────────┘ └┘ └┘ ┴
src └──────┘ └────────────┘ └┘
typ └┘ └──────┘ └┘ └┘ ┴ └────────────┘ └┘ └┘ ┴
641 [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
src └─────────────┘ └────────────┘ └┘
typ ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
642 {f : Π₀ i₁, β₁ i₁} {g : Π i₁, β₁ i₁ → Π₀ i, β i} :
id └┘ └┘┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴┴ ┴ ┴
src └┘ ┴ └┘ ┴
typ └┘ └┘┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴┴ ┴ ┴
643 (f.sum g).support ⊆ f.support.bind (λi, (g i (f i)).support) :=
id ┴└──┘ ┴ └─────┘ ┴ ┴└──────┘└───┘ ┴ ┴ ┴ ┴ ┴ └─────┘
src └──┘ └─────┘ ┴ └──────┘└───┘ └─────┘
typ ┴└──┘ ┴ └─────┘ ┴ ┴└──────┘└───┘ ┴ ┴ ┴ ┴ ┴ └─────┘
doc └──┘ └───┘
644 have ∀i₁ : ι, f.sum (λ (i : ι₁) (b : β₁ i), (g i b) i₁) ≠ 0 →
id ┴ ┴└──┘ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴
src └──┘ ┴
typ ┴ ┴└──┘ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴
doc └──┘
645 (∃ (i : ι₁), f i ≠ 0 ∧ ¬ (g i (f i)) i₁ = 0),
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
646 from assume i₁ h,
id └┘ ┴
typ └┘ ┴
647 let ⟨i, hi, ne⟩ := finset.exists_ne_zero_of_sum_ne_zero h in
id └─┘ ┴ └┘ └┘ └──────────────────────────────────┘ ┴
src └┘ └──────────────────────────────────┘
typ └─┘ ┴ └┘ └┘ └──────────────────────────────────┘ ┴
648 ⟨i, (f.mem_support_iff i).mp hi, ne⟩,
id ┴└──────────────┘ └┘
src └──────────────┘ └┘
typ ┴└──────────────┘ └┘
649 by simpa [finset.subset_iff, mem_support_iff, finset.mem_bind, sum_apply] using this
id └───────────────┘ └─────────────┘ └─────────────┘ └───────┘ └──┘
src └─────┘└───────────────┘└┘└─────────────┘└┘└─────────────┘└┘└───────┘└──────┘ └
typ └─────┘└───────────────┘└┘└─────────────┘└┘└─────────────┘└┘└───────┘└──────┘└──┘└
doc └─────┘ └┘ └┘ └┘ └──────┘ └
txt └─────┘ └┘ └┘ └┘ └──────┘ └
par └─────┘ └┘ └┘ └┘ └──────┘ └
pid ┴┴ └┘ └┘ └┘ ┴┴└────┘ └
st └──────────────────────────────────────────────────────────────────────────────────
650
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
651 @[simp] lemma sum_zero [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
src └─────────────┘ └────────────┘ └┘
typ ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
doc └──┘
652 [add_comm_monoid γ] {f : Π₀ i, β i} :
id └─────────────┘ ┴ └┘ ┴┴ ┴ ┴
src └─────────────┘ └┘ ┴
typ └─────────────┘ ┴ └┘ ┴┴ ┴ ┴
653 f.sum (λi b, (0 : γ)) = 0 :=
id ┴└──┘ ┴ ┴ ┴ ┴
src └──┘ ┴
typ ┴└──┘ ┴ ┴ ┴ ┴
doc └──┘
654 finset.sum_const_zero
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
655
656 @[simp] lemma sum_add [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
src └─────────────┘ └────────────┘ └┘
typ ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
doc └──┘
657 [add_comm_monoid γ] {f : Π₀ i, β i} {h₁ h₂ : Π i, β i → γ} :
id └─────────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ └┘ ┴
typ └─────────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
658 f.sum (λi b, h₁ i b + h₂ i b) = f.sum h₁ + f.sum h₂ :=
id ┴└──┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└──┘ └┘ ┴ ┴└──┘ └┘
src └──┘ ┴ ┴ └──┘ ┴ └──┘
typ ┴└──┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└──┘ └┘ ┴ ┴└──┘ └┘
doc └──┘ └──┘ └──┘
659 finset.sum_add_distrib
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
660
661 @[simp] lemma sum_neg [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
src └─────────────┘ └────────────┘ └┘
typ ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
doc └──┘
662 [add_comm_group γ] {f : Π₀ i, β i} {h : Π i, β i → γ} :
id └────────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────┘ └┘ ┴
typ └────────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
663 f.sum (λi b, - h i b) = - f.sum h :=
id ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴
src └──┘ ┴ ┴ ┴ └──┘
typ ┴└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴
doc └──┘ └──┘
664 f.support.sum_hom (@has_neg.neg γ _)
id ┴└──────┘└──────┘ └─────────┘ ┴
src └──────┘└──────┘ └─────────┘
typ ┴└──────┘└──────┘ └─────────┘ ┴
665
666 @[to_additive]
doc └─────────┘
667 lemma prod_add_index [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
src └─────────────┘ └────────────┘ └┘
typ ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
668 [comm_monoid γ] {f g : Π₀ i, β i}
id └─────────┘ ┴ └┘ ┴┴ ┴ ┴
src └─────────┘ └┘ ┴
typ └─────────┘ ┴ └┘ ┴┴ ┴ ┴
669 {h : Π i, β i → γ} (h_zero : ∀i, h i 0 = 1) (h_add : ∀i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
670 (f + g).prod h = f.prod h * g.prod h :=
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴└───┘ ┴
src ┴ └──┘ ┴ └───┘ ┴ └───┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴└───┘ ┴
doc └──┘ └───┘ └───┘
671 have f_eq : (f.support ∪ g.support).prod (λi, h i (f i)) = f.prod h,
id ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
src └──────┘ ┴ └──────┘ └──┘ ┴ └───┘
typ ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
doc └──┘ └───┘
672 from (finset.prod_subset (finset.subset_union_left _ _) $
id └────────────────┘ └──────────────────────┘
src └────────────────┘ └──────────────────────┘
typ └────────────────┘ └──────────────────────┘
673 by simp [mem_support_iff, h_zero] {contextual := tt}).symm,
id └─────────────┘ └────┘ └┘ └──┘
src └────┘└─────────────┘└┘ └┘ └────────────┘└┘┴ └──┘
typ └────┘└─────────────┘└┘└────┘└┘ └────────────┘└┘┴ └──┘
doc └────┘ └┘ └┘ └────────────┘ ┴
txt └────┘ └┘ └┘ └────────────┘ ┴
par └────┘ └┘ └┘ └────────────┘ ┴
pid ┴┴ └┘ ┴┴ └────────────┘ ┴
st └────────────────────────────────────────────────┘
674 have g_eq : (f.support ∪ g.support).prod (λi, h i (g i)) = g.prod h,
id ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
src └──────┘ ┴ └──────┘ └──┘ ┴ └───┘
typ ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───┘ ┴
doc └──┘ └───┘
675 from (finset.prod_subset (finset.subset_union_right _ _) $
id └────────────────┘ └───────────────────────┘
src └────────────────┘ └───────────────────────┘
typ └────────────────┘ └───────────────────────┘
676 by simp [mem_support_iff, h_zero] {contextual := tt}).symm,
id └─────────────┘ └────┘ └┘ └──┘
src └────┘└─────────────┘└┘ └┘ └────────────┘└┘┴ └──┘
typ └────┘└─────────────┘└┘└────┘└┘ └────────────┘└┘┴ └──┘
doc └────┘ └┘ └┘ └────────────┘ ┴
txt └────┘ └┘ └┘ └────────────┘ ┴
par └────┘ └┘ └┘ └────────────┘ ┴
pid ┴┴ └┘ ┴┴ └────────────┘ ┴
st └────────────────────────────────────────────────┘
677 calc (f + g).support.prod (λi, h i ((f + g) i)) =
id ┴ ┴ ┴ └─────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─────┘ └──┘ ┴
typ ┴ ┴ ┴ └─────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
678 (f.support ∪ g.support).prod (λi, h i ((f + g) i)) :
id ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └──────┘ └──┘ ┴
typ ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
679 finset.prod_subset support_add $
id └────────────────┘ └─────────┘
src └────────────────┘ └─────────┘
typ └────────────────┘ └─────────┘
680 by simp [mem_support_iff, h_zero] {contextual := tt}
id └─────────────┘ └────┘ └┘
src └────┘└─────────────┘└┘ └┘ └────────────┘└┘└─
typ └────┘└─────────────┘└┘└────┘└┘ └────────────┘└┘└─
doc └────┘ └┘ └┘ └────────────┘ └─
txt └────┘ └┘ └┘ └────────────┘ └─
par └────┘ └┘ └┘ └────────────┘ └─
pid ┴┴ └┘ ┴┴ └────────────┘ ┴└
st └──────────────────────────────────────────────────
681 ... = (f.support ∪ g.support).prod (λi, h i (f i)) *
id ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
src ─┘ └──────┘ ┴ └──────┘ └──┘ ┴
typ ─┘ ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ─┘ └──┘
txt ─┘
par ─┘
pid ─┘
st ─┘
682 (f.support ∪ g.support).prod (λi, h i (g i)) :
id ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └──────┘ └──┘
typ ┴└──────┘ ┴ ┴└──────┘ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
683 by simp [h_add, finset.prod_mul_distrib]
id └───┘ └─────────────────────┘
src └────┘ └┘└─────────────────────┘└─
typ └────┘└───┘└┘└─────────────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └──────────────────────────────────────
684 ... = _ : by rw [f_eq, g_eq]
id └──┘ └──┘
src ─┘ └──┘ └┘ └─
typ ─┘ └──┘└──┘└┘└──┘└─
doc ─┘ └──┘ └┘ └─
txt ─┘ └──┘ └┘ └─
par ─┘ └──┘ └┘ └─
pid ─┘ └┘ └┘ ┴└
st ─┘ └───────┘└────┘┴└
685
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
686 lemma sum_sub_index [Π i, add_comm_group (β i)] [Π i, decidable_pred (eq (0 : β i))]
id ┴ └────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
src └────────────┘ └────────────┘ └┘
typ ┴ └────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
687 [add_comm_group γ] {f g : Π₀ i, β i}
id └────────────┘ ┴ └┘ ┴┴ ┴ ┴
src └────────────┘ └┘ ┴
typ └────────────┘ ┴ └┘ ┴┴ ┴ ┴
688 {h : Π i, β i → γ} (h_sub : ∀i b₁ b₂, h i (b₁ - b₂) = h i b₁ - h i b₂) :
id ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
689 (f - g).sum h = f.sum h - g.sum h :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴└──┘ ┴
src ┴ └─┘ ┴ └──┘ ┴ └──┘
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴└──┘ ┴
doc └─┘ └──┘ └──┘
690 have h_zero : ∀i, h i 0 = 0,
id ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴
691 from assume i,
id ┴
typ ┴
692 have h i (0 - 0) = h i 0 - h i 0, from h_sub i 0 0,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴
693 by simpa using this,
id └──┘
src └──────────┘
typ └──────────┘└──┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └───────────────┘
694 have h_neg : ∀i b, h i (- b) = - h i b,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
695 from assume i b,
id ┴ ┴
typ ┴ ┴
696 have h i (0 - b) = h i 0 - h i b, from h_sub i 0 b,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
697 by simpa [h_zero] using this,
id └────┘ └──┘
src └─────┘ └──────┘
typ └─────┘└────┘└──────┘└──┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └────────────────────────┘
698 have h_add : ∀i b₁ b₂, h i (b₁ + b₂) = h i b₁ + h i b₂,
id ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
src ┴ ┴ ┴
typ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
699 from assume i b₁ b₂,
id ┴ └┘ └┘
typ ┴ └┘ └┘
700 have h i (b₁ - (- b₂)) = h i b₁ - h i (- b₂), from h_sub i b₁ (-b₂),
id ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └───┘ ┴ └┘ ┴└┘
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └───┘ ┴ └┘ ┴└┘
701 by simpa [h_neg] using this,
id └───┘ └──┘
src └─────┘ └──────┘
typ └─────┘└───┘└──────┘└──┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └───────────────────────┘
702 by simp [@sum_add_index ι β _ γ _ _ _ f (-g) h h_zero h_add];
id └───────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ └────┘ └───┘
src └────┘ └───────────┘┴ ┴ └─┘ └─────┘ ┴ ┴ └┘ ┴ ┴ ┴
typ └────┘ └───────────┘┴┴┴┴└─┘┴└─────┘┴┴ ┴┴└┘┴┴└────┘┴└───┘┴
doc └────┘ ┴ ┴ └─┘ └─────┘ ┴ └┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ └─┘ └─────┘ ┴ └┘ ┴ ┴ ┴
par └────┘ ┴ ┴ └─┘ └─────┘ ┴ └┘ ┴ ┴ ┴
pid ┴┴ ┴ ┴ └─┘ └─────┘ ┴ └┘ ┴ ┴ ┴
st └───────────────────────────────────────────────────────────
703 simp [@sum_neg_index ι β _ γ _ _ _ g h h_zero, h_neg];
id └───────────┘ ┴ ┴ ┴ ┴ ┴ └────┘ └───┘
src └────┘ └───────────┘┴ ┴ └─┘ └─────┘ ┴ ┴ └┘ ┴
typ └────┘ └───────────┘┴┴┴┴└─┘┴└─────┘┴┴┴┴└────┘└┘└───┘┴
doc └────┘ ┴ ┴ └─┘ └─────┘ ┴ ┴ └┘ ┴
txt └────┘ ┴ ┴ └─┘ └─────┘ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ └─┘ └─────┘ ┴ ┴ └┘ ┴
pid ┴┴ ┴ ┴ └─┘ └─────┘ ┴ ┴ └┘ ┴
st ───────────────────────────────────────────────────────
704 simp [@sum_neg ι β _ γ _ _ _ g h]
id └─────┘ ┴ ┴ ┴ ┴ ┴
src └────┘ └─────┘┴ ┴ └─┘ └─────┘ ┴ └─
typ └────┘ └─────┘┴┴┴┴└─┘┴└─────┘┴┴┴└─
doc └────┘ ┴ ┴ └─┘ └─────┘ ┴ └─
txt └────┘ ┴ ┴ └─┘ └─────┘ ┴ └─
par └────┘ ┴ ┴ └─┘ └─────┘ ┴ └─
pid ┴┴ ┴ ┴ └─┘ └─────┘ ┴ ┴└
st ──────────────────────────────────
705
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
706 @[to_additive]
doc └─────────┘
707 lemma prod_finset_sum_index {γ : Type w} {α : Type x}
708 [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
src └─────────────┘ └────────────┘ └┘
typ ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
709 [comm_monoid γ] [decidable_eq α]
id └─────────┘ ┴ └──────────┘ ┴
src └─────────┘ └──────────┘
typ └─────────┘ ┴ └──────────┘ ┴
710 {s : finset α} {g : α → Π₀ i, β i}
id └────┘ ┴ ┴ └┘ ┴┴ ┴ ┴
src └────┘ └┘ ┴
typ └────┘ ┴ ┴ └┘ ┴┴ ┴ ┴
doc └────┘
711 {h : Π i, β i → γ} (h_zero : ∀i, h i 0 = 1) (h_add : ∀i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
712 s.prod (λi, (g i).prod h) = (s.sum g).prod h :=
id ┴└───┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴└──┘ ┴ └──┘ ┴
src └───┘ └──┘ ┴ └──┘ └──┘
typ ┴└───┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴└──┘ ┴ └──┘ ┴
doc └───┘ └──┘ └──┘
713 finset.induction_on s
id └─────────────────┘ ┴
src └─────────────────┘
typ └─────────────────┘ ┴
doc └─────────────────┘
714 (by simp [prod_zero_index])
id └─────────────┘
src └────┘└─────────────┘┴
typ └────┘└─────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────────────────┘
715 (by simp [prod_add_index, h_zero, h_add] {contextual := tt})
id └────────────┘ └────┘ └───┘ └┘
src └────┘└────────────┘└┘ └┘ └┘ └────────────┘└┘┴
typ └────┘└────────────┘└┘└────┘└┘└───┘└┘ └────────────┘└┘┴
doc └────┘ └┘ └┘ └┘ └────────────┘ ┴
txt └────┘ └┘ └┘ └┘ └────────────┘ ┴
par └────┘ └┘ └┘ └┘ └────────────┘ ┴
pid ┴┴ └┘ └┘ ┴┴ └────────────┘ ┴
st └──────────────────────────────────────────────────────┘
716
717 @[to_additive]
doc └─────────┘
718 lemma prod_sum_index {ι₁ : Type u₁} [decidable_eq ι₁] {β₁ : ι₁ → Type v₁}
id └──────────┘ └┘ └┘
src └──────────┘
typ └──────────┘ └┘ └┘
719 [Π i₁, has_zero (β₁ i₁)] [Π i, decidable_pred (eq (0 : β₁ i))]
id └┘ └──────┘ └┘ └┘ ┴ └────────────┘ └┘ └┘ ┴
src └──────┘ └────────────┘ └┘
typ └┘ └──────┘ └┘ └┘ ┴ └────────────┘ └┘ └┘ ┴
720 [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
src └─────────────┘ └────────────┘ └┘
typ ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
721 [comm_monoid γ]
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
722 {f : Π₀ i₁, β₁ i₁} {g : Π i₁, β₁ i₁ → Π₀ i, β i}
id └┘ └┘┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴┴ ┴ ┴
src └┘ ┴ └┘ ┴
typ └┘ └┘┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴┴ ┴ ┴
723 {h : Π i, β i → γ} (h_zero : ∀i, h i 0 = 1) (h_add : ∀i b₁ b₂, h i (b₁ + b₂) = h i b₁ * h i b₂) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
724 (f.sum g).prod h = f.prod (λi b, (g i b).prod h) :=
id ┴└──┘ ┴ └──┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
src └──┘ └──┘ ┴ └───┘ └──┘
typ ┴└──┘ ┴ └──┘ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
doc └──┘ └──┘ └───┘ └──┘
725 (prod_finset_sum_index h_zero h_add).symm
id └───────────────────┘ └────┘ └───┘ └──┘
src └───────────────────┘ └──┘
typ └───────────────────┘ └────┘ └───┘ └──┘
726
727 @[simp] lemma sum_single [Π i, add_comm_monoid (β i)]
id ┴ └─────────────┘ ┴ ┴
src └─────────────┘
typ ┴ └─────────────┘ ┴ ┴
doc └──┘
728 [Π i, decidable_pred (eq (0 : β i))] {f : Π₀ i, β i} :
id ┴ └────────────┘ └┘ ┴ ┴ └┘ ┴┴ ┴ ┴
src └────────────┘ └┘ └┘ ┴
typ ┴ └────────────┘ └┘ ┴ ┴ └┘ ┴┴ ┴ ┴
729 f.sum single = f :=
id ┴└──┘ └────┘ ┴ ┴
src └──┘ └────┘ ┴
typ ┴└──┘ └────┘ ┴ ┴
doc └──┘
730 begin
st └─────
731 apply dfinsupp.induction f, {rw [sum_zero_index]},
id └────────────────┘ ┴ └────────────┘
src └────┘└────────────────┘┴ └──┘└────────────┘┴
typ └────┘└────────────────┘┴┴ └──┘└────────────┘┴
doc └────┘ ┴ └──┘ ┴
txt └────┘ ┴ └──┘ ┴
par └────┘ ┴ └──┘ ┴
pid ┴ ┴ └┘ ┴
st ───────────────────────────┘└─────┘└────────────┘└─┘└
732 intros i b f H hb ih,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └────────────┘
st ─────────────────────┘└─
733 rw [sum_add_index, ih, sum_single_index],
id └───────────┘ └┘ └──────────────┘
src └──┘└───────────┘└┘ └┘└──────────────┘┴
typ └──┘└───────────┘└┘└┘└┘└──────────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ──────────────────┘└──┘└────────────────┘┴
734 all_goals { intros, simp }
src ┴
typ ┴
doc ┴
txt ┴
par ┴
pid ┴
st ┴
735 end
st └─┘
736
737 @[to_additive]
doc └─────────┘
738 lemma prod_subtype_domain_index [Π i, has_zero (β i)] [Π i, decidable_pred (eq (0 : β i))]
id ┴ └──────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
src └──────┘ └────────────┘ └┘
typ ┴ └──────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
739 [comm_monoid γ] {v : Π₀ i, β i} {p : ι → Prop} [decidable_pred p]
id └─────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────────────┘ ┴
src └─────────┘ └┘ ┴ └────────────┘
typ └─────────┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────────────┘ ┴
740 {h : Π i, β i → γ} (hp : ∀x∈v.support, p x) :
id ┴ ┴ ┴ ┴ ┴ ┴└──────┘ ┴ ┴
src └──────┘
typ ┴ ┴ ┴ ┴ ┴ ┴└──────┘ ┴ ┴
741 (v.subtype_domain p).prod (λi b, h i.1 b) = v.prod h :=
id ┴└─────────────┘ ┴ └──┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴└───┘ ┴
src └─────────────┘ └──┘ ┴ ┴ └───┘
typ ┴└─────────────┘ ┴ └──┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴└───┘ ┴
doc └─────────────┘ └──┘ └───┘
742 finset.prod_bij (λp _, p.val)
id └─────────────┘ ┴ ┴ ┴└──┘
src └─────────────┘ └──┘
typ └─────────────┘ ┴ ┴ ┴└──┘
743 (by simp)
744 (by simp)
745 (assume ⟨a₀, ha₀⟩ ⟨a₁, ha₁⟩, by simp)
id ┴ ┴
typ ┴ ┴
746 (λ i hi, ⟨⟨i, hp i hi⟩, by simpa using hi, rfl⟩)
id ┴ └┘ ┴ └┘ ┴ └┘ └┘ └─┘
src └─┘
typ ┴ └┘ ┴ └┘ ┴ └┘ └┘ └─┘
st ┴ └┘
747
748 lemma subtype_domain_sum [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
src └─────────────┘ └────────────┘ └┘
typ ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
749 {s : finset γ} {h : γ → Π₀ i, β i} {p : ι → Prop} [decidable_pred p] :
id └────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ └────────────┘ ┴
src └────┘ └┘ ┴ └────────────┘
typ └────┘ ┴ ┴ └┘ ┴┴ ┴ ┴ ┴ └────────────┘ ┴
doc └────┘
750 (s.sum h).subtype_domain p = s.sum (λc, (h c).subtype_domain p) :=
id ┴└──┘ ┴ └────────────┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴ └────────────┘ ┴
src └──┘ └────────────┘ ┴ └──┘ └────────────┘
typ ┴└──┘ ┴ └────────────┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴ └────────────┘ ┴
doc └────────────┘ └────────────┘
751 eq.symm (s.sum_hom _)
id └─────┘ ┴└──────┘
src └─────┘ └──────┘
typ └─────┘ ┴└──────┘
752
753 lemma subtype_domain_finsupp_sum {δ : γ → Type x} [decidable_eq γ]
id ┴ └──────────┘ ┴
src └──────────┘
typ ┴ └──────────┘ ┴
754 [Π c, has_zero (δ c)] [Π c, decidable_pred (eq (0 : δ c))]
id ┴ └──────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
src └──────┘ └────────────┘ └┘
typ ┴ └──────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
755 [Π i, add_comm_monoid (β i)] [Π i, decidable_pred (eq (0 : β i))]
id ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
src └─────────────┘ └────────────┘ └┘
typ ┴ └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ ┴ ┴
756 {p : ι → Prop} [decidable_pred p]
id ┴ └────────────┘ ┴
src └────────────┘
typ ┴ └────────────┘ ┴
757 {s : Π₀ c, δ c} {h : Π c, δ c → Π₀ i, β i} :
id └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴
src └┘ ┴ └┘ ┴
typ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴
758 (s.sum h).subtype_domain p = s.sum (λc d, (h c d).subtype_domain p) :=
id ┴└──┘ ┴ └────────────┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ └────────────┘ ┴
src └──┘ └────────────┘ ┴ └──┘ └────────────┘
typ ┴└──┘ ┴ └────────────┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ └────────────┘ ┴
doc └──┘ └────────────┘ └──┘ └────────────┘
759 subtype_domain_sum
760
761 end prod_and_sum
762
763 end dfinsupp